index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
/
genarg.mli
Age
Commit message (
Expand
)
Author
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-09-10
[dune] Add apidoc target using `odoc`
Emilio Jesus Gallego Arias
2018-03-08
Make most of TACTIC EXTEND macros runtime calls.
Maxime Dénès
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-06-09
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-05-04
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-04-08
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-03-30
Ensuring that the type of base generic arguments contain triples.
Pierre-Marie Pédrot
2016-03-19
Removing dead code in Genarg.
Pierre-Marie Pédrot
2016-03-19
Removing the untyped representation of genargs.
Pierre-Marie Pédrot
2016-03-17
Removing the registering of default values for generic arguments.
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
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-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
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-17
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-12
Removing dead unsafe code in Genarg.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-08-29
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-02-27
Remove unsafe code (Obj.magic) in Tacinterp.
Arnaud Spiwack
2014-01-19
Adding a default object to generic argument registering mechanism.
Pierre-Marie Pédrot
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-08-04
Small cleaning of printing coercion failures in Ltac interpretation.
ppedrot
2013-07-05
Removing SortArgType.
ppedrot
2013-07-05
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-06-30
Using functors to reduce the boilerplate used in registering
ppedrot
2013-06-27
Getting rid of IntroPatternArgType.
ppedrot
2013-06-21
Splitted up Genarg in four different levels:
ppedrot
