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