aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.mli
Commit message (Expand)AuthorAge
...
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* correction de bug dans Function et augmentation de la classe des fonctions su...Gravatar jforest2007-05-17
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Une passe sur l'injection et la discrimination...Gravatar herbelin2006-10-01
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* Réparation bug #1004; nettoyageGravatar herbelin2005-09-08
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Restructuration fonctions de réécriture depuis égalité dépendante; facto...Gravatar herbelin2004-10-27
* Simplifications concommitantes à la correction du bug #855Gravatar herbelin2004-09-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...Gravatar herbelin2004-03-11
* Ajout 'replace in'Gravatar herbelin2004-03-01
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Death of 'a somewhat cryptic module'Gravatar herbelin2003-10-11
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
* nouveau Subst:Gravatar barras2002-12-17
* Subst (tout court)Gravatar filliatr2002-09-16
* tactique Subst x1 ... xnGravatar filliatr2002-09-11
* Code mort de AutoRewriteGravatar herbelin2002-09-09
* AutoRewrite substitutive...Gravatar coq2002-08-13
* tactique SubstGravatar filliatr2002-07-17
* Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...Gravatar herbelin2002-06-05
* Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...Gravatar herbelin2002-06-05
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* entetesGravatar filliatr2001-03-15