aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
Commit message (Expand)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
* Define rec_declaration in terms of prec_declaration.Gravatar SimonBoulier2018-06-05
* Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Safer VM interfacesGravatar Maxime Dénès2018-01-26
* Fix order of let-in representation comment.Gravatar Jasper Hugunin2017-12-19
* [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
* COMMENT: Constr.kind_of_termGravatar Matej Kosik2016-10-26
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2016-01-11
* | COMMENTS: added to the "Constr.case_info" type.Gravatar Matej Kosik2015-12-18
* | COMMENTS: added to some variants of the "Constr.kind_of_term" type.Gravatar Matej Kosik2015-12-18
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Gravatar Arnaud Spiwack2015-02-24
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* Update infer_conv to record trivial Prop <= Type i constraints that are neede...Gravatar Matthieu Sozeau2014-05-26
* Add doc on the new API for universe polymorphism and primitive projectionsGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* Adding a [fold_map] operation on constrs.Gravatar Pierre-Marie Pédrot2014-04-24
* Removing generic hashes in kernel.Gravatar Pierre-Marie Pédrot2014-03-03
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 23:25:58 +0000