index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
autorewrite.ml
Commit message (
Expand
)
Author
Age
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.
msozeau
2008-04-12
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...
herbelin
2006-09-21
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
Correction bug #1097 (dû à une typo...)
herbelin
2006-03-02
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Implemented autorewrite with ... in hyp [using ...].
sacerdot
2005-05-18
*
Réparation incompatibilité de comportement introduite lors de mise en compa...
herbelin
2004-11-22
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
Added code to get rid of duplicate rewriting rules.
sacerdot
2004-10-28
*
Compatibilité de Hint Rewrite avec Write State
herbelin
2004-10-13
*
Nouvelle en-tête
herbelin
2004-07-16
*
Globalisation des hints autorewrite
herbelin
2003-10-20
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Oops...
coq
2002-10-01
*
Table fonctionnelle dans autorewrite
coq
2002-10-01
*
AutoRewrite substitutive...
coq
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
compat ocaml 3.03
filliatr
2001-12-13
*
Transparent
barras
2001-09-20
*
Fonction lookup enlevee
delahaye
2001-04-19
*
entetes
filliatr
2001-03-15
*
AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disque
delahaye
2000-12-19
*
Portage d'AutoRewrite
delahaye
2000-12-02