| Age | Commit message (Expand) | Author |
|---|
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann |
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l... | Maxime Dénès |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert |
| 2017-04-09 | Documenting how the recursive indices of a fixpoint are computed. | Hugo Herbelin |
| 2017-03-31 | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot |
| 2016-11-08 | Introducing a new EConstr.t type to perform the nf_evar operation on demand. | Pierre-Marie Pédrot |
| 2016-03-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-03-22 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2016-03-22 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | COMMENTS: of "Constr.case_info" type were updated. | Matej Kosik |
| 2015-12-18 | COMMENTS: added to the "Constr.case_info" type. | Matej Kosik |
| 2015-10-06 | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin |
| 2015-08-02 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin |
| 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 |
