aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/nsatz.ml
Commit message (Expand)AuthorAge
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
* Merge PR#532: Clean Nsatz implementation.Gravatar Maxime Dénès2017-04-11
|\
| * Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Splitting the nsatz ML module into an implementation and a grammar files.Gravatar Pierre-Marie Pédrot2016-03-06