Same for Fin

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15648 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2706: Coqide and layout that use special modifiers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15649 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix eta contraction in Reductionops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15650 85f007b7-540e-0410-9357-904b9bb8a0f7
documentation of bullets (forward port from v8.4).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15654 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing #2836 (materialize_evar might refine as a side effect the
current evar to project; this may happen if this evar is dependent and
is involved in evar-evar conversion problem eventually solved by
instantiating the current evar; could maybe be optimized when the evar
to materialize has invertible instance in which case
define_evar_from_virtual_equation applied on the current evar could be
shortcut, avoiding to create an evar).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
Better fixing propagation of carry in sub_mult used for euclidian
division over unbounded integers (thanks again to L. Théry for
pointing out the remaining problem in r15637).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15659 85f007b7-540e-0410-9357-904b9bb8a0f7
Bigint: avoid dependency over Pp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15664 85f007b7-540e-0410-9357-904b9bb8a0f7
Bigint : better ensure canonicity of arrays of int blocks

In the chosen representation of negative numbers, (-base) is
actually legal as first element of an int array. This situation
was wrongly handled by many functions in this module, leading to
possible non-canonical representation of a big number, and hence
faulty "equal" answers or buggy output of "to_string".

For instance, on a 32-bit machine :

open Big_int;;
to_string (sub (of_string "-10000") (of_string "-1000000"));;
(* was displaying 9810000 instead of 990000 *)

Also simplified "of_string", which now rely on "neg" for handling
negative numbers.

Btw, improved checks comparing w.r.t OCaml's Big_int instead of float.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15665 85f007b7-540e-0410-9357-904b9bb8a0f7
Bigint: adds a missing -1 in hugo's last commit 15659

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15666 85f007b7-540e-0410-9357-904b9bb8a0f7
Bigint: new functions of_int and to_int, 2nd arg of pow in int

 * Many of_string and to_string could be replaced by of_int and to_int
   when the number isn't too large. NB: to_int may raise a Failure
   if the number is larger than max_int.

 * In numbers_syntax, computing the height of bigN trees via bigint
   is *really* overkill, int should be enough there : this limits
   printable/parsable bigN to (2^31)^(2^max_int) ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7
re-sync CHANGES with 8.4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15672 85f007b7-540e-0410-9357-904b9bb8a0f7
Document the command Add/Remove Search Blacklist

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15675 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "Fixing include printers"

If you add Auto to dev/printers.mllib, then you have to add Tacmach, so
you have to add Redexpr, consequently Vnorm is required, it depends on
Vm, that include externals !
Let's revert commit 15675.

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

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15677 85f007b7-540e-0410-9357-904b9bb8a0f7
More entries in the index

Patch by Adam Chilipala.

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

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqdoc: More keywords, better special char escape, special case for "in *"

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15680 85f007b7-540e-0410-9357-904b9bb8a0f7
Dump references in reduction tactics

Patch by Adam Chilipala.

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

Patch by Adam Chilipala.

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