MSetRBT: a tail-recursive plength

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15688 85f007b7-540e-0410-9357-904b9bb8a0f7
Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) markup/typesetting to coqdoc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqdoc inlined verbatim_char in latex

Patch by Adam Chilipala.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
Vecnacentries.dump_global silently ignores exceptions

So PrintName and Extraction dump globals when they exist

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15691 85f007b7-540e-0410-9357-904b9bb8a0f7
configure: two minor fixes for win32

 * ocamlc -version may end with a \r in win32 (fix #2849)

 * $COQSRC may initially be cygwin-specific and hence rejected by ocaml.
   For the moment, an ad-hoc fix is to remove the problematic $COQSRC,
   and mark the -src option as incompatible with win32...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15696 85f007b7-540e-0410-9357-904b9bb8a0f7
Avoid Pp.std_ppcmds in Misctypes.sort_info

 Otherwise, after a Set Printing Universes we may end on
 a comparison of Pp.std_ppcmds, which may fail on functional
 values (cf. Constrextern.check_same_type), as notice by Pierre-Marie

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15697 85f007b7-540e-0410-9357-904b9bb8a0f7
Updating credits for final 8.4

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15700 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixup for macOS 10.8 & Ocaml 4.0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15704 85f007b7-540e-0410-9357-904b9bb8a0f7
More standard layout for \lambda in chapter CIC.

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

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15709 85f007b7-540e-0410-9357-904b9bb8a0f7
Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
Unification in Evar_conv uses an abstract machine state

It uses a term in front of a stack instead of a term in front of a list of applied
terms. From outside of eq_appr_x nothing should have changed.

Nasty evar instantiation bug

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

Coqide used the wrong escape sequence to delimit coq phrases.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15720 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2861 : ocamlopt but no lablgtk2.cmxa problem

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15721 85f007b7-540e-0410-9357-904b9bb8a0f7
fast bitwise operations (lor,land,lxor) on int31 and BigN

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
Improving rendering of ...-separated lists and sequences in reference
manual (making style uniform: no {\tt \ldots}; using only one space
when there is no delimiters in the sequence).

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