index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
extratactics.mli
Age
Commit message (
Expand
)
Author
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-12-27
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-11-30
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-02
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2012-12-14
Modulification of identifier
ppedrot
2012-10-15
Continue killing hidden tactics : no more generated h_xxx
letouzey
2012-08-08
Updating headers.
herbelin
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-12-21
Generic support for open terms in tactics
herbelin
2008-06-21
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2007-05-20
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2006-08-22
+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no
jforest
2006-06-23
Correction ident -> hyp pour dinterpréter des identificateurs devant êt...
herbelin
2006-05-02
Extension syntaxique de rewrite in: au lieu de pouvoir faire
letouzey
2006-03-21
+ destruct now works as induction on multiple arguments :
jforest
2005-01-21
Compatibilité ocamlweb pour cible doc
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2002-06-05
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-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin