aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-01-23Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.ppedrot
2012-01-23Bug 739: forbid dumpglob while using Coqtop in interactive modepboutill
2012-01-21Coqtop and coqc: cleaning description of options in RefMan and manpages.pboutill
2012-01-20Added documentation for "r foo" in Ltac debugger.herbelin
2012-01-20Added documentation for "Set Parsing Explicit" + fixed mistakenlyherbelin
2012-01-20Breakpoints in Ltac debugger: new command "r foo" to jump to the nextherbelin
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2012-01-20Notations with binders: Accepting using notations for functional termsherbelin
2012-01-20Reverted previous commit, which broke library compilation.ppedrot
2012-01-20This is a quick hack to permit the parsing of the locality flag in the Progra...ppedrot
2012-01-20Fix printing of classesmsozeau
2012-01-19Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.msozeau
2012-01-19Added the btauto tactic to the documentation.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 05:27:07 +0000