aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\
* | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
* | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
|\ \
| | * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| |/ |/|
| * Documenting how the recursive indices of a fixpoint are computed.Gravatar Hugo Herbelin2017-04-09
* | Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* | Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2016-01-11
* | COMMENTS: added to the "Constr.case_info" type.Gravatar Matej Kosik2015-12-18
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
|/
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Gravatar Arnaud Spiwack2015-02-24
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* 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
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 06:43:09 +0000