| Commit message (Expand) | Author | Age |
|---|
| * | Add (almost) compatibility with camlp4, without breaking support for camlp5 |  letouzey | 2010-05-19 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Here comes the commit, announced long ago, of the new tactic engine. |  aspiwack | 2010-04-22 |
| * | Fixed bug #2999 (destruct was not refreshing universes of what it generalized *) |  herbelin | 2010-04-20 |
| * | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin | 2010-04-14 |
| * | Update CHANGES, add documentation for new commands/tactics and do a bit |  msozeau | 2010-01-30 |
| * | New version of 12650 that was broken (supporting again records when | herbelin | 2010-01-12 |
| * | revert commit 12650 for the moment, since it breaks MSetAVL | letouzey | 2010-01-12 |
| * | Temporary fix to compensate the loss of descent on dependent | herbelin | 2010-01-12 |
| * | Fixing bug #2146 (broken selection of occurrences in "change"). | herbelin | 2009-12-30 |
| * | Improving descend_in_conjunctions (using a combinators instead of a tactic) | herbelin | 2009-12-29 |
| * | In "simpl c" and "change c with d", c can be a pattern. | herbelin | 2009-12-24 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | Made the side-conditions of lemmas always come last when chaining "apply in" | herbelin | 2009-12-13 |
| * | Fix bug in typeclass resolution. Better handling of universes in | msozeau | 2009-12-01 |
| * | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau | 2009-11-24 |
| * | Promote evar_defs to evar_map (in Evd) |  glondu | 2009-11-11 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
| * | - Fix discharge bug in typeclasses: some constrs were not actually | msozeau | 2009-11-06 |
| * | Misc fixes. | msozeau | 2009-11-06 |
| * | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
| * | Restore (and test) broken chaining of lemmas in "apply in" in presence | herbelin | 2009-10-25 |
| * | Add support for remaining side-conditions in "apply in as". | herbelin | 2009-10-25 |
| * | Changed the way to support compatibility with previous versions. | herbelin | 2009-10-04 |
| * | Removal of trailing spaces. |  serpyc | 2009-10-04 |
| * | Added option "Unset Dependent Propositions Elimination" to protect | herbelin | 2009-10-03 |
| * | Delay the choice of eliminator in destruct/induction until we know if | herbelin | 2009-09-27 |
| * | Only one "in" clause in "destruct" even for a multiple "destruct". | herbelin | 2009-09-20 |
| * | - Fixed a bug in checking that implicit arguments are all correctly | herbelin | 2009-09-18 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin | 2009-09-10 |
| * | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
| * | - Add more precise error localisation when one of the application fails | herbelin | 2009-08-04 |
| * | Added "etransitivity". | herbelin | 2009-08-03 |
| * | 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 |
| * | Reimplementation of leibniz rewrite to control the instantiation of the | msozeau | 2009-06-16 |
| * | - 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 |
| * | Minor unification changes: | msozeau | 2009-05-18 |
| * | - Allowing multiple calls to tactic fix with automatic generation of | herbelin | 2009-05-17 |
| * | Backporting 12080 (fixing bug #2091 on bad rollback in the "where" | herbelin | 2009-04-24 |
| * | Fix premature optimisation in dependent induction: even variable args need | msozeau | 2009-04-10 |
| * | Fix auto so that Extern tactics associated to no patterns can apply to | msozeau | 2009-03-31 |
| * | Compromise wrt introduction-names compatibility issue after addition | herbelin | 2009-03-22 |
| * | Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl) | herbelin | 2009-03-17 |
| * | Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4" | herbelin | 2009-03-16 |
| * | Cleaning/uniformizing the interface of tacticals.mli | herbelin | 2009-03-14 |
| * | Add support for dependent "destruct" over terms in dependent types. | herbelin | 2009-02-23 |
letouzey
aspiwack
herbelin
msozeau
glondu
serpyc