index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrarg.ml
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-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
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-19
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
Removing the registering of default values for generic arguments.
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
2016-01-17
Temporary commit getting rid of Obj.magic unsafety for Genarg.
Pierre-Marie Pédrot
2016-01-14
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
Removing ident and var generic arguments.
Pierre-Marie Pédrot
2015-12-28
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-21
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Pierre-Marie Pédrot
2015-12-21
Removing the now useless genarg generic argument.
Pierre-Marie Pédrot
2015-12-17
Getting rid of some hardwired generic arguments.
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-05
Fix [uconstr] name for argextend.
Arnaud Spiwack
2014-07-29
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-04-14
Closing bug #3260
Julien Forest
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-12-19
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-01
Removing RefArgType generic argument.
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-05
Removing SortArgType.
ppedrot
2013-07-02
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-06-27
Getting rid of IntroPatternArgType.
ppedrot
2013-06-21
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
