| Age | Commit message (Expand) | Author |
|---|
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot |
| 2015-04-22 | Tactical `progress` compares term up to potentially equalisable universes. | Arnaud Spiwack |
| 2015-02-24 | New function [Constr.equal_with] to compare terms up to variants of [kind_of_... | Arnaud Spiwack |
| 2015-02-24 | Refactoring in [Constr]. | Arnaud Spiwack |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-17 | Ensuring the good invariants of hashcons table generation in the API. | Pierre-Marie Pédrot |
| 2014-12-17 | Fix (actually, properly implement :) hashconsing of projections, | Matthieu Sozeau |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-07-31 | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-05-26 | Update infer_conv to record trivial Prop <= Type i constraints that are neede... | Matthieu Sozeau |
| 2014-05-08 | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau |
| 2014-05-06 | Add missing case for primitive projection in fold_map. | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | Cleanup in constr, correct classification of polymorphic defs. | Matthieu Sozeau |
| 2014-05-06 | - Fix index-list to show computational relations for rewriting files. | Matthieu Sozeau |
| 2014-05-06 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-28 | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin |
| 2014-04-24 | Adding a [fold_map] operation on constrs. | Pierre-Marie Pédrot |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-03-03 | Removing generic hashes in kernel. | Pierre-Marie Pédrot |
| 2014-03-02 | Fixing generic Hashtbl.hash in Constr. | Pierre-Marie Pédrot |
| 2013-11-04 | Using allocation-free version of Array higher-order function in critical | ppedrot |
| 2013-10-27 | More sharing in Constr.map_with_binders. | ppedrot |
| 2013-10-24 | Specializing hash functions for widely used types. | ppedrot |
| 2013-10-22 | Various optimizations in Constr, such as term sharing and allocation | ppedrot |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-08-22 | More complete hashcons : lists (dirpath), arrays (constr) | letouzey |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
