| Age | Commit message (Expand) | Author |
|---|
| 2012-01-23 | Fix for Program Instance not separately checking the resolution of evars of t... | msozeau |
| 2012-01-23 | Another quick hack that works this time, to handle printing of locality in Pr... | ppedrot |
| 2012-01-23 | Deleted the only use of BeginSubProof from the standard library. | ppedrot |
| 2012-01-23 | Removed a seemingly unused argument in Require of modules, introduced 10 year... | ppedrot |
| 2012-01-23 | Fixed pretty-printing of Opaque, Transparent and Strategy locality flags. | ppedrot |
| 2012-01-23 | Bug 739: forbid dumpglob while using Coqtop in interactive mode | pboutill |
| 2012-01-21 | Coqtop and coqc: cleaning description of options in RefMan and manpages. | pboutill |
| 2012-01-20 | Added documentation for "r foo" in Ltac debugger. | herbelin |
| 2012-01-20 | Added documentation for "Set Parsing Explicit" + fixed mistakenly | herbelin |
| 2012-01-20 | Breakpoints in Ltac debugger: new command "r foo" to jump to the next | herbelin |
| 2012-01-20 | Added new command "Set Parsing Explicit" for deactivating parsing (and | herbelin |
| 2012-01-20 | Notations with binders: Accepting using notations for functional terms | herbelin |
| 2012-01-20 | Reverted previous commit, which broke library compilation. | ppedrot |
| 2012-01-20 | This is a quick hack to permit the parsing of the locality flag in the Progra... | ppedrot |
| 2012-01-20 | Fix printing of classes | msozeau |
| 2012-01-19 | Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}. | msozeau |
| 2012-01-19 | Added the btauto tactic to the documentation. | ppedrot |
| 2012-01-19 | Pretty printing of generalized binder | pboutill |
| 2012-01-19 | Boolean Option Patterns Compatibility | pboutill |
| 2012-01-19 | No more use of tauto in Init/ | pboutill |
| 2012-01-17 | Fixed the pretty-printing of the Program plugin. | ppedrot |
| 2012-01-17 | Makefile: fix make distclean w.r.t. test-suite | letouzey |
| 2012-01-17 | MSetAVL: better implementation of filter suggested by X. Leroy | letouzey |
| 2012-01-17 | Some fix in beautify pretty-printer | pboutill |
| 2012-01-16 | Parameters in pattern first step. | pboutill |
| 2012-01-16 | Inductiveops.nb_*{,_env} cleaning | pboutill |
| 2012-01-16 | Bug 2679: Do not try to install cmxs with -byte-only | pboutill |
| 2012-01-16 | Bug 2676: ./configure --prefix shoudn't ask for a config directory. | pboutill |
| 2012-01-16 | make mli-doc fix | pboutill |
| 2012-01-14 | coq_micromega.ml: fix order of recursive calls to rconstant | glondu |
| 2012-01-14 | Add distclean back to test-suite/Makefile | glondu |
| 2012-01-14 | More newlines in debugging output of psatzl | glondu |
| 2012-01-13 | Added a Btauto plugin, that solves boolean tautologies. | ppedrot |
| 2012-01-13 | Added the decidability of (<=) on nat. | ppedrot |
| 2012-01-12 | Fix typo | glondu |
| 2012-01-10 | Fix printing of instances, generalized arguments. | msozeau |
| 2012-01-07 | Fix typo | glondu |
| 2012-01-06 | Fixed the itarget of the previous commit... | ppedrot |
| 2012-01-06 | Added a typeclass-based system to reason on decidable propositions. | ppedrot |
| 2012-01-06 | Forbids (as it has always been the behaviour) to have two different open | aspiwack |
| 2012-01-06 | Fixes bug #2654 (tactic instantiate failing to update existential variables). | aspiwack |
| 2012-01-05 | Backtracking on r14876 (fix for bug #2267): extra scopes might be | herbelin |
| 2012-01-04 | Fixing Arguments Scope bug when too many scopes are given (bug #2667). | herbelin |
| 2012-01-04 | Type inference unification: fixed a 8.4 bug in the presence of unification | herbelin |
| 2012-01-03 | Makefile.doc: attempt to solve race condition for creating doc/refman/html. | herbelin |
| 2011-12-27 | Bug 2669 and more: make full-stdlib | pboutill |
| 2011-12-26 | Coqdoc: Fixing missing newline when using "Proof term." | herbelin |
| 2011-12-26 | Reference Manual: misc fixes (spelling, index, updating pre-8.0 syntax). | herbelin |
| 2011-12-26 | update CHANGES w.r.t. simpl | gareuselesinge |
| 2011-12-25 | Version number, copyright, credits: missing updates. | herbelin |
