index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
/
genarg.mli
Commit message (
Expand
)
Author
Age
*
Make most of TACTIC EXTEND macros runtime calls.
Maxime Dénès
2018-03-08
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Switching to an untyped toplevel representation for Ltac values.
Pierre-Marie Pédrot
2016-05-04
*
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-04-08
*
Ensuring that the type of base generic arguments contain triples.
Pierre-Marie Pédrot
2016-03-30
*
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-19
*
Removing the untyped representation of genargs.
Pierre-Marie Pédrot
2016-03-19
*
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Moving val_cast to Tacinterp.
Pierre-Marie Pédrot
2016-01-17
*
|
Getting rid of the awkward unpack mechanism from Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Simplification and type-safety of Pcoq thanks to GADTs in Genarg.
Pierre-Marie Pédrot
2016-01-17
*
|
Exporting Genarg implementation in the API.
Pierre-Marie Pédrot
2016-01-17
*
|
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
*
|
Finer-grained types for toplevel values.
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-21
*
|
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
*
|
Attaching a dynamic argument to the toplevel type of generic arguments.
Pierre-Marie Pédrot
2015-12-21
*
|
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
*
|
Removing dead unsafe code in Genarg.
Pierre-Marie Pédrot
2015-12-12
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Type-safe version of genarg list / pair / opt functions.
Pierre-Marie Pédrot
2014-08-29
*
Simplification of Genarg unpackers.
Pierre-Marie Pédrot
2014-08-29
*
Remove unsafe code (Obj.magic) in Tacinterp.
Arnaud Spiwack
2014-02-27
*
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
2014-01-19
*
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
*
Small cleaning of printing coercion failures in Ltac interpretation.
ppedrot
2013-08-04
*
Removing SortArgType.
ppedrot
2013-07-05
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Using functors to reduce the boilerplate used in registering
ppedrot
2013-06-30
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
Maxime Dénès
Théo Zimmermann
Matej Košík
Pierre-Marie Pédrot
Arnaud Spiwack
ppedrot