index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
extraargs.mli
Commit message (
Expand
)
Author
Age
*
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-04-24
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
*
Work on the "occurrences" tactic argument. It is now possible to pass
msozeau
2008-04-20
*
Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.
msozeau
2008-04-12
*
Add occurence extra arg
msozeau
2008-01-30
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Bug in replace tactics introduced in r9073 (overlap between replace .. with a...
jforest
2006-08-23
*
Forgot a file in previous commit
jforest
2006-08-22
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Hugly temporary notation
sacerdot
2004-09-29
*
New: (temporary) concrete syntax to specify the morphism signature:
sacerdot
2004-09-24
*
Nouvelle en-tête
herbelin
2004-07-16
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
Code obsolete
herbelin
2003-11-08
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29