index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
extratactics.mli
Commit message (
Expand
)
Author
Age
*
Modulification of identifier
ppedrot
2012-12-14
*
Continue killing hidden tactics : no more generated h_xxx
letouzey
2012-10-15
*
Updating headers.
herbelin
2012-08-08
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-08-22
*
Correction ident -> hyp pour dinterpréter des identificateurs devant êt...
herbelin
2006-06-23
*
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-05-02
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Nouvelle en-tête
herbelin
2004-07-16
*
Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...
herbelin
2002-06-05
*
Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...
herbelin
2002-06-05
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29