Equality: avoid some unprotected List.nth (fix #2837)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16393 85f007b7-540e-0410-9357-904b9bb8a0f7
- Fix caching of local hint database in typeclasses eauto which could
miss some hypotheses.
- Fix automatic solving of obligation in program, which was not trying
to solve obligations that had no undefined dependencies left.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16394 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Backporting Matthieu's trunk commit r16134 (eta was missing in
Flexible/Rigid and SemiFlexible/Rigid conversion problems). This
commit solved bug #3023. Also added regression test for this bug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16410 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: updating CHANGES

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16412 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Like in r16346, do not filter local definitions (here in the
type-based second-order unification algorithm).

In type-based second-order unification algorithm, protect local
definitions in instances of evars to wrongly be considered as
potentially flexible.

Altogether, this fixes the anomaly in #3003 (even if some additional
work has to be done to improve the resulting error message, see next
commit).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16416 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix #3001 (rename arg of global cst inside section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16424 85f007b7-540e-0410-9357-904b9bb8a0f7
Only arguments declared as implicit can be renamed

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16425 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing typo in r16410 (backport of r16134)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16428 85f007b7-540e-0410-9357-904b9bb8a0f7
coqc: accept -exclude-dir option (fix #3025)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16433 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqdep: add an -exclude-dir option (wish mentionned in #3025)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16434 85f007b7-540e-0410-9357-904b9bb8a0f7
test-suite : avoid messages about undefined $(bogomips) in BSD

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16436 85f007b7-540e-0410-9357-904b9bb8a0f7
Favor Pp.msg_warn (with flush) over Pp.warning (without), fixing #3013

 Without flush, the warning could arrive *after* an error message,
 leading ProofGeneral to think that the last sentence has been successful.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16437 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing bug #2230. Was actually fixed in trunk by side-effect of
commit r16422.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16459 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Added a unit test for bug #2230.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16461 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Hack to solve a "Bad recursive type" anomaly.

Retyping expects its argument already well-typed. However, if
unification problems are not fully solved, a term to match can have an
evar type together with the constraint that this evar has to be
convertible to some given inductive type.

One could have tried to have a more eager resolution of unification
constraint but I'm afraid of the cost in comparing c=c' in general in
"?x[c] = c'" unification problems, so I instead added a hack in
retyping to recover the constraint.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16472 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Little fix for Nsatz: hypotheses not directly relevant to the nsatz
problem are cleared (in case they denote applicative terms with at
least 6 arguments). However some of them are used for type class
instance inference (e.g. hypotheses of type Integral_domain).

This commits prevents clearing these hypotheses.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16484 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Protection against "Bad recursive type" in w_unify0 (bug #3036).

Morally, unification wants to unify "fun x:Meta => Meta"
with "fun x:nat => match x with ... end". Retyping is asked to
type "match x with ... end" in the context "x:Meta" where the
type of x has de facto been lost. Retyping fails.

I don't see an easy remedy since w_unify0 builds the unifier
lazily, and I'm not sure it is worth to propagate the unifier to
retyping so that it knows it. After all, the call to retyping in
w_unify0 is not so critical.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16490 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing buggy commit r16490 (supposed to fix bug #3036).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16505 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Fixing a typo in the documentation of discriminate.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16552 85f007b7-540e-0410-9357-904b9bb8a0f7