index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
constrarg.mli
Commit message (
Expand
)
Author
Age
*
Honor parsing and printing levels for tactic entry in TACTIC EXTEND and
Hugo Herbelin
2016-04-27
*
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
*
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-27
*
|
Changing the toplevel type of the int_or_var generic type to int.
Pierre-Marie Pédrot
2015-12-21
*
|
Removing the now useless genarg generic argument.
Pierre-Marie Pédrot
2015-12-21
|
/
*
grammar: export hypident
Enrico Tassi
2015-03-30
*
Update headers.
Maxime Dénès
2015-01-12
*
Lazy interpretation of patterns so that expressions such as "intros H H'/H"
Hugo Herbelin
2014-08-18
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
[uconstr]: use a closure instead of eager substitution.
Arnaud Spiwack
2014-08-06
*
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-07-29
*
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-05-22
*
Closing bug #3260
Julien Forest
2014-04-14
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21