aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
Commit message (Expand)AuthorAge
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* 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
* Fast-path equality of sorts in compare_constr*Gravatar Matthieu Sozeau2014-05-08
* Add missing case for primitive projection in fold_map.Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* Cleanup in constr, correct classification of polymorphic defs.Gravatar Matthieu Sozeau2014-05-06
* - Fix index-list to show computational relations for rewriting files.Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar 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
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing generic hashes in kernel.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing generic Hashtbl.hash in Constr.Gravatar Pierre-Marie Pédrot2014-03-02
* Using allocation-free version of Array higher-order function in criticalGravatar ppedrot2013-11-04
* More sharing in Constr.map_with_binders.Gravatar ppedrot2013-10-27
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
* Various optimizations in Constr, such as term sharing and allocationGravatar ppedrot2013-10-22
* 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
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* More complete hashcons : lists (dirpath), arrays (constr)Gravatar letouzey2013-08-22
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 14:09:05 +0000