| Age | Commit message (Expand) | Author |
|---|
| 2009-09-13 | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin |
| 2009-09-11 | Generalized the possibility to refer to a global name by a notation | herbelin |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 2009-09-09 | Allow setoid rewrite to rewrite in pattern-matching scrutinees or | msozeau |
| 2009-09-09 | Stop trying to search if the relation is declared as a [RewriteRelation] | msozeau |
| 2009-09-08 | Fix the bug-ridden code used to choose leibniz or generalized | msozeau |
| 2009-09-03 | Support globality flag properly for "Add Morphism foo : foo_mor" syntax. | msozeau |
| 2009-09-02 | Stop unnecessary use of lazy values for constraints, simplifying | msozeau |
| 2009-08-13 | Death of "survive_module" and "survive_section" (the first one was | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-08-06 | Move out JMeq of subst for compatibility (it affects e.g. the | herbelin |
| 2009-08-04 | - Add more precise error localisation when one of the application fails | herbelin |
| 2009-08-04 | Fixed subst failing when a truly heterogeneous JMeq hyp is in the | herbelin |
| 2009-08-03 | Added "etransitivity". | herbelin |
| 2009-08-02 | Improved parameterization of Coq: | herbelin |
| 2009-08-02 | Fixed a typo in "info" for tactic "right". | herbelin |
| 2009-07-24 | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey |
| 2009-07-14 | Simplify eauto and fix it for compatibility, allowing full delta during | msozeau |
| 2009-07-09 | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau |
| 2009-07-08 | Simplify addition of hints to a hint_db. Rebuild the dnet associated | msozeau |
| 2009-07-08 | Reactivation of pattern unification of evars in apply unification, in | herbelin |
| 2009-07-07 | Jolification : tentative de supprimer les "( evd)" et associés qui | aspiwack |
| 2009-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-06-28 | Raise an error and not an anomaly if a rewrite is attempted on a | msozeau |
| 2009-06-22 | Correct treatment of dependent products in signatures: create the evars | msozeau |
| 2009-06-18 | Fix "unsatisfiable constraints" error messages to include all the | msozeau |
| 2009-06-16 | Reimplementation of leibniz rewrite to control the instantiation of the | msozeau |
| 2009-06-11 | Use a lazy value for the message in FailError, so that it won't be | msozeau |
| 2009-06-11 | When typing a non-dependent arrow, do not put the (anonymous) variable | msozeau |
| 2009-06-10 | Use the projections for reflexivity, symmetry and transitivity proofs to | msozeau |
| 2009-06-09 | Correct handling of the initial existentials from the goal and the ones | msozeau |
| 2009-06-08 | Do a fixpoint on the result of typeclass search to force the | msozeau |
| 2009-06-07 | - Added two new introduction patterns with the following temptative syntaxes: | herbelin |
| 2009-06-06 | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin |
| 2009-06-01 | ## Lines starting with '## ' will be removed from the log message. | msozeau |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2009-05-18 | Minor unification changes: | msozeau |
| 2009-05-17 | - Allowing multiple calls to tactic fix with automatic generation of | herbelin |
| 2009-05-16 | Minor fixes in typeclasses: | msozeau |
| 2009-05-10 | - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-05-05 | Improvements in typeclasses eauto and generalized rewriting: | msozeau |
| 2009-04-28 | Fixes for bugs in r12110: | msozeau |
| 2009-04-27 | Cleanup old eauto code. | msozeau |
| 2009-04-27 | - Implementation of a new typeclasses eauto procedure based on success | msozeau |
| 2009-04-27 | - Fixed a little bug in previous commit (bad failure in case of unknown entry). | herbelin |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
| 2009-04-24 | Backporting 12080 (fixing bug #2091 on bad rollback in the "where" | herbelin |
| 2009-04-24 | Fixing bug #2308 ("instantiate" tactic did not comply with | herbelin |
| 2009-04-21 | Rename [Morphism] into [Proper] and [respect] into [proper] to comply | msozeau |
