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
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Fixing bug #2732 (anomaly when using the tolerance for writing
herbelin
2012-03-18
*
Noise for nothing
pboutill
2012-03-02
*
Rename the "raw" argument extension into "glob"
glondu
2010-12-27
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Export printing functions for extra arguments. Maybe there's a way to
msozeau
2010-08-03
*
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
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
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