aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
* Ensuring that the type of base generic arguments contain triples.Gravatar Pierre-Marie Pédrot2016-03-30
* Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-30
* Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-19
* Removing the untyped representation of genargs.Gravatar Pierre-Marie Pédrot2016-03-19
* Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Moving val_cast to Tacinterp.Gravatar Pierre-Marie Pédrot2016-01-17
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Reimplementing Genarg safely.Gravatar Pierre-Marie Pédrot2016-01-17
* | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | Finer-grained types for toplevel values.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing ad-hoc interpretation rules for tactic notations and their genarg.Gravatar Pierre-Marie Pédrot2015-12-21
* | Sharing toplevel representation for several generic types.Gravatar Pierre-Marie Pédrot2015-12-21
* | Removing the now useless genarg generic argument.Gravatar Pierre-Marie Pédrot2015-12-21
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | Attaching a dynamic argument to the toplevel type of generic arguments.Gravatar Pierre-Marie Pédrot2015-12-21
* | Getting rid of some hardwired generic arguments.Gravatar Pierre-Marie Pédrot2015-12-17
* | Removing dead unsafe code in Genarg.Gravatar Pierre-Marie Pédrot2015-12-12
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Small cleaning of printing coercion failures in Ltac interpretation.Gravatar ppedrot2013-08-04
* Removing SortArgType.Gravatar ppedrot2013-07-05
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Using functors to reduce the boilerplate used in registeringGravatar ppedrot2013-06-30
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21