aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/autorewrite.ml
Commit message (Expand)AuthorAge
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...Gravatar herbelin2006-09-21
* + Changing "in <hyp>" to "in <clause>" (no at, no InValue and noGravatar jforest2006-08-22
* Correction bug #1097 (dû à une typo...)Gravatar herbelin2006-03-02
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* 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