| Commit message (Expand) | Author | Age |
|---|
| * | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules |  glondu | 2010-09-30 |
| * | Remove some occurrences of "open Termops" | glondu | 2010-09-28 |
| * | Some dead code removal, thanks to Oug analyzer |  letouzey | 2010-09-24 |
| * | Updated all headers for 8.3 and trunk |  herbelin | 2010-07-24 |
| * | Adding the destauto tactic, that reduces match by destructing matched |  courtieu | 2010-07-22 |
| * | Finish adding out-of-the-box support for camlp4 | letouzey | 2010-07-09 |
| * | Made "replace" accepts open terms on its left-hand-side. | herbelin | 2010-06-28 |
| * | Added Chung-Kil Hur's smart "pattern" tactic (h_resolve). | herbelin | 2010-06-22 |
| * | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
| * | Update CHANGES, add documentation for new commands/tactics and do a bit |  msozeau | 2010-01-30 |
| * | Generic support for open terms in tactics | herbelin | 2009-12-21 |
| * | Updated compatibility for rewriting equality proofs that are dependent | herbelin | 2009-12-12 |
| * | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau | 2009-11-24 |
| * | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
| * | This big commit addresses two problems: |  soubiran | 2009-10-21 |
| * | Remove useless Liboject.export_function field | glondu | 2009-09-17 |
| * | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
| * | 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 |
| * | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey | 2009-07-24 |
| * | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau | 2009-06-30 |
| * | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin | 2009-05-20 |
| * | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin | 2009-05-09 |
| * | Rewrite autorewrite to use a dnet indexed by the left-hand sides (or | msozeau | 2009-04-14 |
| * | Getting rid of the previous implementation of setoid_rewrite which was | msozeau | 2009-01-18 |
| * | Finish fix for the treatment of [inverse] in [setoid_rewrite], making a | msozeau | 2008-12-16 |
| * | About "apply in": | herbelin | 2008-12-09 |
| * | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau | 2008-11-05 |
| * | Fixes and refinements regarding occurrence selection: | herbelin | 2008-10-26 |
| * | Various little improvements: | msozeau | 2008-09-25 |
| * | Évolutions diverses et variées. | herbelin | 2008-08-04 |
| * | Fixes in generalize_eqs/dependent induction to allow the user to specify | msozeau | 2008-07-28 |
| * | New tactics [conv] to test convertibility (actually, unification) of two | msozeau | 2008-07-22 |
| * | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin | 2008-06-21 |
| * | Correction du bug des types singletons pas sous-type de Set | herbelin | 2008-04-27 |
| * | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
| * | Nettoyage de code en vue de la release. Plus de Warning: Unused |  aspiwack | 2007-12-18 |
| * | Adding the tactic "instantiate" (without argument), to force the | glondu | 2007-12-07 |
| * | Factorisation des opérations sur le type option de Util dans un module | aspiwack | 2007-12-05 |
| * | Add a new tactic to generalize an instantiated inductive predicate adding equ... | msozeau | 2007-08-07 |
| * | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin | 2007-05-22 |
| * | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin | 2007-05-20 |
| * | Processor integers + Print assumption (see coqdev mailing list for the | aspiwack | 2007-05-11 |
| * | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin | 2007-04-28 |
| * | Correction bug #1041 (double cause : non évitement des noms existants en | herbelin | 2006-12-12 |
| * | Ajout de la tactique "apply in". | herbelin | 2006-10-24 |
| * | Une passe sur l'injection et la discrimination... | herbelin | 2006-10-01 |
| * | Bug in replace tactics introduced in r9073 (overlap between replace .. with a... |  jforest | 2006-08-23 |
| * | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest | 2006-08-22 |
glondu
letouzey
herbelin
courtieu
msozeau
soubiran
aspiwack
jforest