aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-07-20Reductionops refactoringpboutill
2012-07-20Fixup implicits in patterns & notationspboutill
2012-07-20Vector equalities first stuffpboutill
2012-07-20Put Option in Clibpboutill
2012-07-20Fixing test-suitepboutill
2012-07-20Let coqtop be a little more stupid in hint answer: otherwise, thatppedrot
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
2012-07-18Various minor fixes to coqdoc from A. Chlipala.msozeau
2012-07-16Added abstration layer to goal display in CoqIDE, and cleaned partsppedrot
2012-07-16Fixing goal display when still focussing but no more goals.ppedrot
2012-07-13Display the "unjustified" information returned by coqtop.ppedrot
2012-07-13Fixes r15610 (A new status Unsafe in Interface).aspiwack
2012-07-12flex_maybeflex factoringpboutill
2012-07-12miller_pfenning unification code factoringpboutill
2012-07-12flex_kind_of_term does not have a copy of termpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 20:36:18 +0000