Fix: tooltip correctly handles the absence of info (empty string)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix compilation (vernac.ml, missing ;)

I did forget a ; while dealing with conflicts in git-svn rebase

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16460 85f007b7-540e-0410-9357-904b9bb8a0f7
Splitting Term into five unrelated interfaces:

1. sorts.ml: A small file utility for sorts;

2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;

3. vars.ml: Everything related to term variables, that is, occurences
and substitution;

4. context.ml: Rel/Named context and all that;

5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
Merging Context and Sign.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix wrong computation of dependency signature in cases raising an uncaught exception later.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16464 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing a redundant function from Evd.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
Reporting the change on matching partial applications in patterns of
the form "_ pat1 ... patn", and considering it experimental at this
stage.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16466 85f007b7-540e-0410-9357-904b9bb8a0f7
Relaxing the constraint on eta-expanding on the fly while looking for
notation to use at printing time. We now allow to print "sigT P" as
"{x:_ & P x}", generating a "_" for the missing type, when the notation
is defined by 'Notation "{ x : A  & P }" := (sigT (fun x:A => P))'.

Do better, and change the notation to "(sigT (A:=A) (fun x => P))" so
that the type is known even when eta-expansion is needed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16467 85f007b7-540e-0410-9357-904b9bb8a0f7
Improvement of r16204 on reporting tactic error locations: if the main
error is not located, then do not use locations from Tactic Notation
(TacAlias) or TACTIC EXTEND (TacExtend) code since they are relative
to the defining code of these extensions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16468 85f007b7-540e-0410-9357-904b9bb8a0f7
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/trunk@16469 85f007b7-540e-0410-9357-904b9bb8a0f7
Now printing body of abbreviations (i.e. notation with a name) with
full usage of notations instead of the previous cheap way to prevent
circularity in printing by deactivating all notations.

(Since "->" became a notation, printing abbreviations without
notations at all had become even more inconvenient).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
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/trunk@16471 85f007b7-540e-0410-9357-904b9bb8a0f7
Improving printing of 'rew' notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16473 85f007b7-540e-0410-9357-904b9bb8a0f7