aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.ml
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-12-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: move Tactypes to proofsEmilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-02Do not identify a pre_ident as a string Ltac value.Hugo Herbelin
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-22Clarifying the interpretation path for the "constr_with_binding" argument.Hugo Herbelin
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-03-19Removing dead code in Genarg.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic entries defined by Coq itself.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-19Moving wit_unit to Stdarg.ppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot