aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/autorewrite.ml
Commit message (Expand)AuthorAge
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
* - Fix handling of clauses in setoid_rewrite to rewrite under bindersGravatar msozeau2009-04-17
* Rewrite autorewrite to use a dnet indexed by the left-hand sides (orGravatar msozeau2009-04-14
* Rewrite of setoid_rewrite to modularize it based on proof-producingGravatar msozeau2009-04-13
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* 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