| Commit message (Expand) | Author | Age |
|---|
| * | Remove useless Liboject.export_function field |  glondu | 2009-09-17 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | - Inductive types in the "using" option of auto/eauto/firstorder are |  herbelin | 2009-09-13 |
| * | Generalized the possibility to refer to a global name by a notation | herbelin | 2009-09-11 |
| * | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin | 2009-09-10 |
| * | 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-09 |
| * | Fix the bug-ridden code used to choose leibniz or generalized | msozeau | 2009-09-08 |
| * | Support globality flag properly for "Add Morphism foo : foo_mor" syntax. | msozeau | 2009-09-03 |
| * | Stop unnecessary use of lazy values for constraints, simplifying | msozeau | 2009-09-02 |
| * | Death of "survive_module" and "survive_section" (the first one was | herbelin | 2009-08-13 |
| * | - 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-06 |
| * | - 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-04 |
| * | Added "etransitivity". | herbelin | 2009-08-03 |
| * | Improved parameterization of Coq: | herbelin | 2009-08-02 |
| * | Fixed a typo in "info" for tactic "right". | herbelin | 2009-08-02 |
| * | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" |  letouzey | 2009-07-24 |
| * | Simplify eauto and fix it for compatibility, allowing full delta during | msozeau | 2009-07-14 |
| * | Use the proper unification flags in e_exact. This makes exact fail a bit | msozeau | 2009-07-09 |
| * | 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-08 |
| * | Jolification : tentative de supprimer les "( evd)" et associés qui |  aspiwack | 2009-07-07 |
| * | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau | 2009-06-30 |
| * | Raise an error and not an anomaly if a rewrite is attempted on a | msozeau | 2009-06-28 |
| * | Correct treatment of dependent products in signatures: create the evars | msozeau | 2009-06-22 |
| * | Fix "unsatisfiable constraints" error messages to include all the | msozeau | 2009-06-18 |
| * | Reimplementation of leibniz rewrite to control the instantiation of the | msozeau | 2009-06-16 |
| * | 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-11 |
| * | Use the projections for reflexivity, symmetry and transitivity proofs to | msozeau | 2009-06-10 |
| * | Correct handling of the initial existentials from the goal and the ones | msozeau | 2009-06-09 |
| * | Do a fixpoint on the result of typeclass search to force the | msozeau | 2009-06-08 |
| * | - Added two new introduction patterns with the following temptative syntaxes: | herbelin | 2009-06-07 |
| * | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin | 2009-06-06 |
| * | ## Lines starting with '## ' will be removed from the log message. | msozeau | 2009-06-01 |
| * | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin | 2009-05-20 |
| * | Minor unification changes: | msozeau | 2009-05-18 |
| * | - Allowing multiple calls to tactic fix with automatic generation of | herbelin | 2009-05-17 |
| * | Minor fixes in typeclasses: | msozeau | 2009-05-16 |
| * | - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it | herbelin | 2009-05-10 |
| * | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin | 2009-05-09 |
| * | Improvements in typeclasses eauto and generalized rewriting: | msozeau | 2009-05-05 |
| * | Fixes for bugs in r12110: | msozeau | 2009-04-28 |
| * | 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-27 |
| * | Backporting 12080 (fixing bug #2091 on bad rollback in the "where" | herbelin | 2009-04-24 |
glondu
herbelin
msozeau
letouzey
aspiwack