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
Fix typo in manual

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16474 85f007b7-540e-0410-9357-904b9bb8a0f7
Close the .glob file after having saved .vo

This is a no op for standard Coq, but is important for
Paral-ITP, since saving the library to disk forces all
frozen computations, and some of them may spit out glob
data, so the file descriptor must be valid.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16475 85f007b7-540e-0410-9357-904b9bb8a0f7
Ideutils: comment on missing Glib utf8 handling function

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

One can freeze/unfreeze a portion of the summary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16477 85f007b7-540e-0410-9357-904b9bb8a0f7
States: frozen states can hold closures

States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values.  The flag is propagated to Lib and Summary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqide: view -> zoom in / out / fit

This commit adds zoom facilities that are useful for demos (quickly
increate font size) and daily use (set size so that 80 colums fit
the window width).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16479 85f007b7-540e-0410-9357-904b9bb8a0f7
New module Xml_printer (dual to Xml_parser)

Code for printing XML moved from xml_utils.ml to xml_printer.ml
and improved to generate less garbage using Buffer.t systematically.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
fake_ide: xml parser does not check for EOF

Exactly as Coqide's parser does.

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