aboutsummaryrefslogtreecommitdiff
path: root/lib/genarg.mli
AgeCommit message (Expand)Author
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-09-10[dune] Add apidoc target using `odoc`Emilio Jesus Gallego Arias
2018-03-08Make most of TACTIC EXTEND macros runtime calls.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-05-04Switching to an untyped toplevel representation for Ltac values.Pierre-Marie Pédrot
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-03-30Ensuring that the type of base generic arguments contain triples.Pierre-Marie Pédrot
2016-03-19Removing dead code in Genarg.Pierre-Marie Pédrot
2016-03-19Removing the untyped representation of genargs.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-17Moving val_cast to Tacinterp.Pierre-Marie Pédrot
2016-01-17Getting rid of the awkward unpack mechanism from Genarg.Pierre-Marie Pédrot
2016-01-17Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Pierre-Marie Pédrot
2016-01-17Exporting Genarg implementation in the API.Pierre-Marie Pédrot
2016-01-17Temporary commit getting rid of Obj.magic unsafety for Genarg.Pierre-Marie Pédrot
2016-01-14Removing constr generic argument.Pierre-Marie Pédrot
2016-01-14Removing ident and var generic arguments.Pierre-Marie Pédrot
2015-12-28Removing the special status of open_constr generic argument.Pierre-Marie Pédrot
2015-12-21Finer-grained types for toplevel values.Pierre-Marie Pédrot
2015-12-21Removing ad-hoc interpretation rules for tactic notations and their genarg.Pierre-Marie Pédrot
2015-12-21Removing the now useless genarg generic argument.Pierre-Marie Pédrot
2015-12-21Using dynamic values in tactic evaluation.Pierre-Marie Pédrot
2015-12-21Attaching a dynamic argument to the toplevel type of generic arguments.Pierre-Marie Pédrot
2015-12-17Getting rid of some hardwired generic arguments.Pierre-Marie Pédrot
2015-12-12Removing dead unsafe code in Genarg.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-08-29Type-safe version of genarg list / pair / opt functions.Pierre-Marie Pédrot
2014-08-29Simplification of Genarg unpackers.Pierre-Marie Pédrot
2014-02-27Remove unsafe code (Obj.magic) in Tacinterp.Arnaud Spiwack
2014-01-19Adding a default object to generic argument registering mechanism.Pierre-Marie Pédrot
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
2013-07-05Removing SortArgType.ppedrot
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-06-30Using functors to reduce the boilerplate used in registeringppedrot
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-21Splitted up Genarg in four different levels:ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:39:38 +0000