index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrarg.mli
Age
Commit message (
Expand
)
Author
2016-09-21
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-15
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-15
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
Pierre-Marie Pédrot
2016-06-18
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-05-04
Removing useless generic arguments.
Pierre-Marie Pédrot
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-04-27
Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"
Hugo Herbelin
2016-04-27
Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...
Hugo Herbelin
2016-04-27
Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"
Hugo Herbelin
2016-04-27
Honor parsing and printing levels for tactic entry in TACTIC EXTEND and
Hugo Herbelin
2016-03-20
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-02-22
The tactic generic argument now returns a value rather than a glob_expr.
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-28
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-27
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-21
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-03-30
grammar: export hypident
Enrico Tassi
2015-01-12
Update headers.
Maxime Dénès
2014-08-18
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-06
[uconstr]: use a closure instead of eager substitution.
Arnaud Spiwack
2014-07-29
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-05-22
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-04-14
Closing bug #3260
Julien Forest
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-02
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2013-12-19
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-11-30
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-07-02
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-06-21
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
