index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
constrarg.ml
Commit message (
Expand
)
Author
Age
*
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
*
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-19
*
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-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
*
|
Temporary commit getting rid of Obj.magic unsafety for Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
Removing ident and var generic arguments.
Pierre-Marie Pédrot
2016-01-14
*
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
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-21
*
|
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
|
/
*
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
*
Fix [uconstr] name for argextend.
Arnaud Spiwack
2014-08-05
*
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-07-29
*
Closing bug #3260
Julien Forest
2014-04-14
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-12-01
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Removing SortArgType.
ppedrot
2013-07-05
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
Pierre-Marie Pédrot
Maxime Dénès
Enrico Tassi
Hugo Herbelin
Arnaud Spiwack
Julien Forest
Pierre Letouzey
ppedrot