aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-08-22Do not forget to build the unicode libraries, necessary to compile and launch...msozeau
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
2012-08-11Some extra INCOMPATIBILITIES since 8.4.herbelin
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-11Some changes in CHANGES.herbelin
2012-08-11Improving rendering of ...-separated lists and sequences in referenceherbelin
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2012-08-10Bug 2861 : ocamlopt but no lablgtk2.cmxa problempboutill
2012-08-10Fixes bug #2857.aspiwack
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-08-08Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.herbelin
2012-08-08Updating version numbers.herbelin
2012-08-08Documenting eta-conversion.herbelin
2012-08-08More standard layout for \lambda in chapter CIC.herbelin
2012-08-08Fixup for macOS 10.8 & Ocaml 4.0pboutill
2012-08-07Typo in r15654herbelin
2012-08-07Updating credits for final 8.4herbelin
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
2012-08-07configure: two minor fixes for win32letouzey
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
2012-08-06Coqdoc inlined verbatim_char in latexpboutill
2012-08-06Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) markup/typese...pboutill
2012-08-06Win32: some quote fixesletouzey
2012-08-06MSetRBT: a tail-recursive plengthletouzey
2012-08-06Try to make the use of Unix.lockf in micromega compatible with Win32letouzey
2012-08-05Dump references in Extractionpboutill
2012-08-05Dump references in reduction tacticspboutill
2012-08-05Coqdoc: More keywords, better special char escape, special case for "in *"pboutill
2012-08-05Dump referencespboutill
2012-08-05More entries in the indexpboutill
2012-08-05Dump references in Resetpboutill
2012-08-05Revert "Fixing include printers"pboutill
2012-08-03Fixing include printersppedrot
2012-08-03Document the command Add/Remove Search Blacklistletouzey
2012-08-03re-sync CHANGES with 8.4letouzey
2012-08-02Bigint: new functions of_int and to_int, 2nd arg of pow in intletouzey
2012-07-31Bigint: adds a missing -1 in hugo's last commit 15659letouzey
2012-07-30Bigint : better ensure canonicity of arrays of int blocksletouzey
2012-07-30Bigint: avoid dependency over Ppletouzey
2012-07-29Better fixing propagation of carry in sub_mult used for euclidianherbelin
2012-07-29Fixing #2836 (materialize_evar might refine as a side effect theherbelin
2012-07-25documentation of bullets (forward port from v8.4).courtieu
2012-07-25Fix eta contraction in Reductionopspboutill
2012-07-25Bug 2706: Coqide and layout that use special modifierspboutill
2012-07-25Same for Finpboutill
2012-07-21Fixing bug #2835 (the rationale for printing notations was notherbelin
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
2012-07-21Fixing unchecked overflow in sub_mult used for euclidian division overherbelin
2012-07-21Slight modification to the printing of goals when in emacs mode.courtieu