| Commit message (Expand) | Author | Age |
* | Merge PR #486: Make some functions on terms more robust w.r.t new term constr... | Maxime Dénès | 2017-11-24 |
|\ |
|
| * | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | 2017-11-23 |
* | | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | 2017-11-22 |
|/ |
|
* | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | 2017-11-06 |
* | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
* | Merge PR#582: Fix warnings | Maxime Dénès | 2017-05-02 |
|\ |
|
* | | More consistent writing of de Bruijn. | Théo Zimmermann | 2017-05-01 |
* | | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | 2017-05-01 |
* | | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l... | Maxime Dénès | 2017-04-28 |
|\ \ |
|
| | * | Fix 4.04 warnings | Gaetan Gilbert | 2017-04-27 |
| |/
|/| |
|
| * | Documenting how the recursive indices of a fixpoint are computed. | Hugo Herbelin | 2017-04-09 |
* | | Make the Constr.kind_of_term type parametric in sorts and universes. | Pierre-Marie Pédrot | 2017-03-31 |
* | | Introducing a new EConstr.t type to perform the nf_evar operation on demand. | Pierre-Marie Pédrot | 2016-11-08 |
|/ |
|
* | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-03-30 |
|\ |
|
| * | 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-03-22 |
* | | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
|\| |
|
| * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
* | | COMMENTS: of "Constr.case_info" type were updated. | Matej Kosik | 2016-01-11 |
* | | COMMENTS: added to the "Constr.case_info" type. | Matej Kosik | 2015-12-18 |
* | | Splitting kernel universe code in two modules. | Pierre-Marie Pédrot | 2015-10-06 |
| * | 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-08-02 |
|/ |
|
* | Tactical `progress` compares term up to potentially equalisable universes. | Arnaud Spiwack | 2015-04-22 |
* | 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-02-24 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | 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-17 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | 2014-10-20 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot | 2014-07-31 |
* | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
* | Update infer_conv to record trivial Prop <= Type i constraints that are neede... | Matthieu Sozeau | 2014-05-26 |
* | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau | 2014-05-08 |
* | 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-05-06 |
* | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin | 2014-04-28 |
* | Adding a [fold_map] operation on constrs. | Pierre-Marie Pédrot | 2014-04-24 |
* | 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-05 |
* | Removing generic hashes in kernel. | Pierre-Marie Pédrot | 2014-03-03 |