aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.mli
Commit message (Expand)AuthorAge
* 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
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* NettoyageGravatar herbelin2000-05-18
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Adaptés pour le type constr_pattern et les nouvelles fonctions de filtrageGravatar herbelin2000-04-30
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Modification de type_of_case, type_case_branches, etc;nettoyageGravatar herbelin2000-03-21
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:27:12 +0000