aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-01-19Pretty printing of generalized binderpboutill
2012-01-19Boolean Option Patterns Compatibilitypboutill
2012-01-19No more use of tauto in Init/pboutill
2012-01-17Fixed the pretty-printing of the Program plugin.ppedrot
2012-01-17Makefile: fix make distclean w.r.t. test-suiteletouzey
2012-01-17MSetAVL: better implementation of filter suggested by X. Leroyletouzey
2012-01-17Some fix in beautify pretty-printerpboutill
2012-01-16Parameters in pattern first step.pboutill
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2012-01-16Bug 2679: Do not try to install cmxs with -byte-onlypboutill
2012-01-16Bug 2676: ./configure --prefix shoudn't ask for a config directory.pboutill
2012-01-16make mli-doc fixpboutill
2012-01-14coq_micromega.ml: fix order of recursive calls to rconstantglondu
2012-01-14Add distclean back to test-suite/Makefileglondu
2012-01-14More newlines in debugging output of psatzlglondu
2012-01-13Added a Btauto plugin, that solves boolean tautologies.ppedrot
2012-01-13Added the decidability of (<=) on nat.ppedrot
2012-01-12Fix typoglondu
2012-01-10Fix printing of instances, generalized arguments.msozeau
2012-01-07Fix typoglondu
2012-01-06Fixed the itarget of the previous commit...ppedrot
2012-01-06Added a typeclass-based system to reason on decidable propositions.ppedrot
2012-01-06Forbids (as it has always been the behaviour) to have two different openaspiwack
2012-01-06Fixes bug #2654 (tactic instantiate failing to update existential variables).aspiwack
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2012-01-03Makefile.doc: attempt to solve race condition for creating doc/refman/html.herbelin
2011-12-27Bug 2669 and more: make full-stdlibpboutill
2011-12-26Coqdoc: Fixing missing newline when using "Proof term."herbelin
2011-12-26Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax).herbelin
2011-12-26update CHANGES w.r.t. simplgareuselesinge
2011-12-25Version number, copyright, credits: missing updates.herbelin
2011-12-23Credits for 8.4: More exhaustive list of external contributors.herbelin
2011-12-23myocamlbuild: -DWIN32 instead of -DWin32letouzey
2011-12-23Configure: the backslashes in win32 paths should be escapedletouzey
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
2011-12-21sequel of previous commitletouzey
2011-12-21Isolate a few types of Goptions in a pure .mli, solving a dep issue with ocam...letouzey
2011-12-21Pure interfaces shouldn't be mentionned in .mllibletouzey
2011-12-21adapt myocamlbuild after changes in coqdep_boot (.beautify)letouzey
2011-12-21Cleaning CHANGES file.herbelin
2011-12-19Notifying removal of accidental unfolding of recursive calls ofherbelin
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
2011-12-19test suite update after r14808pboutill
2011-12-19Bug 2377 part 2: old revision file is erased by installpboutill
2011-12-19Fixed some printing details for dependent evars in emacs mode. Patchcourtieu
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-12-18CoqIde files position is freedesktop compliant.pboutill
2011-12-18./configure & freedesktoppboutill