aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz
Commit message (Expand)AuthorAge
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
* [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* [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
* Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\
* | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| * Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/
* 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 unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
* Fix nsatz not recognizing real literals.Gravatar Guillaume Melquiond2017-04-20
* Merge PR#532: Clean Nsatz implementation.Gravatar Maxime Dénès2017-04-11
|\
| * Fix an algorithmic issue in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| * Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\|
| * Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
| |\
| * | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | * [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
| |/
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/
* Adding interface files to Nsatz ML files.Gravatar Pierre-Marie Pédrot2016-09-28
* Fast russian peasant exponentiation in Nsatz.Gravatar Pierre-Marie Pédrot2016-09-26
* Monomorphizing various uses of arrays in Nsatz.Gravatar Pierre-Marie Pédrot2016-09-26
* Partial fix for bug #5085: nsatz_compute stack overflows.Gravatar Pierre-Marie Pédrot2016-09-26
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
|\
* \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \
| | * improved complexity in nsatzGravatar thery2016-07-06
| | * Bug Fixes : 4851 4858 4880 for nsatzGravatar thery2016-07-06
| |/
| * Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
* | Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | Splitting the nsatz ML module into an implementation and a grammar files.Gravatar Pierre-Marie Pédrot2016-03-06
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19