aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/autorewrite.ml
Commit message (Expand)AuthorAge
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
* Réparation incompatibilité de comportement introduite lors de mise en compa...Gravatar herbelin2004-11-22
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* Added code to get rid of duplicate rewriting rules.Gravatar sacerdot2004-10-28
* Compatibilité de Hint Rewrite avec Write StateGravatar herbelin2004-10-13
* Nouvelle en-têteGravatar herbelin2004-07-16
* Globalisation des hints autorewriteGravatar herbelin2003-10-20
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Oops...Gravatar coq2002-10-01
* Table fonctionnelle dans autorewriteGravatar coq2002-10-01
* AutoRewrite substitutive...Gravatar coq2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* compat ocaml 3.03Gravatar filliatr2001-12-13
* TransparentGravatar barras2001-09-20
* Fonction lookup enleveeGravatar delahaye2001-04-19
* entetesGravatar filliatr2001-03-15
* AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disqueGravatar delahaye2000-12-19
* Portage d'AutoRewriteGravatar delahaye2000-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 18:27:27 +0000