| Age | Commit message (Expand) | Author |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-06-18 | Relaxed the constraint introduced in r14190 that froze the existing | herbelin |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-05-13 | Improved the efficiency of evars traverals thanks to a split of | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-12-28 | Safer, though ad hoc, approach to re-interpretation of the argument of | herbelin |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-16 | adding an option functional_induction_rewrite_dependent to make functional in... | jforest |
| 2009-12-12 | Updated compatibility for rewriting equality proofs that are dependent | herbelin |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-09-08 | Fix the bug-ridden code used to choose leibniz or generalized | msozeau |
| 2009-08-06 | Move out JMeq of subst for compatibility (it affects e.g. the | herbelin |
| 2009-07-24 | Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite" | letouzey |
| 2009-06-30 | Add new variants of [rewrite] and [autorewrite] which differ in the | msozeau |
| 2009-04-08 | Some dead code removal + cleanups | letouzey |
| 2008-11-05 | Port [rewrite] tactics to open terms. Currently no check that evars | msozeau |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-26 | Even better test for choosing rewrite or setoid_rewrite. | msozeau |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-04-12 | Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. | msozeau |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2008-03-01 | Rework on rich forms of rewrite | letouzey |
| 2007-07-06 | Adding a syntax for "n-ary" rewrite: | letouzey |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-20 | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin |
| 2007-05-17 | correction de bug dans Function et augmentation de la classe des fonctions su... | jforest |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2006-10-01 | Une passe sur l'injection et la discrimination... | herbelin |
| 2006-08-22 | + Changing "in <hyp>" to "in <clause>" (no at, no InValue and no | jforest |
| 2006-05-02 | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey |
| 2006-03-21 | + destruct now works as induction on multiple arguments : | jforest |
| 2005-09-08 | Réparation bug #1004; nettoyage | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2004-10-27 | Restructuration fonctions de réécriture depuis égalité dépendante; facto... | herbelin |
| 2004-09-24 | Simplifications concommitantes à la correction du bug #855 | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-11 | Suppression de la distinction entre elimination de Type vers Type ou pas (Fal... | herbelin |
| 2004-03-01 | Ajout 'replace in' | herbelin |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-10-11 | Death of 'a somewhat cryptic module' | herbelin |
| 2003-05-19 | Restructuration des procédures de filtrage | herbelin |
| 2003-03-28 | notations <>, Assumption avec existentiel, replace term | mohring |
| 2002-12-17 | nouveau Subst: | barras |
| 2002-09-16 | Subst (tout court) | filliatr |