index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
autorewrite.mli
Age
Commit message (
Expand
)
Author
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-01
Cleaning Pp.ppnl use
ppedrot
2012-05-29
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-03-02
Noise for nothing
pboutill
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-06-22
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-06-30
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-04-14
Rewrite autorewrite to use a dnet indexed by the left-hand sides (or
msozeau
2009-04-13
Rewrite of setoid_rewrite to modularize it based on proof-producing
msozeau
2006-08-22
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2005-05-18
Implemented autorewrite with ... in hyp [using ...].
sacerdot
2004-11-17
New command "Print Rewrite HindDb dbname".
sacerdot
2004-07-16
Nouvelle en-tête
herbelin
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2001-03-15
entetes
filliatr
2000-12-19
AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disque
delahaye
2000-12-12
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-02
Portage d'AutoRewrite
delahaye