aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.mli
Commit message (Expand)AuthorAge
* 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