aboutsummaryrefslogtreecommitdiff
path: root/kernel/constr.ml
AgeCommit message (Expand)Author
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-09Documenting how the recursive indices of a fixpoint are computed.Hugo Herbelin
2017-03-31Make the Constr.kind_of_term type parametric in sorts and universes.Pierre-Marie Pédrot
2016-11-08Introducing a new EConstr.t type to perform the nf_evar operation on demand.Pierre-Marie Pédrot
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11COMMENTS: of "Constr.case_info" type were updated.Matej Kosik
2015-12-18COMMENTS: added to the "Constr.case_info" type.Matej Kosik
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02A patch renaming equal into eq in the module dealing withHugo Herbelin
2015-08-02Adding eq/compare/hash for syntactic view atHugo Herbelin
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-02-24New function [Constr.equal_with] to compare terms up to variants of [kind_of_...Arnaud Spiwack
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-01-12Update headers.Maxime Dénès
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-17Fix (actually, properly implement :) hashconsing of projections,Matthieu Sozeau
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-07-31Useless export of Instance.eqeq. We hashcons everything before calling thisPierre-Marie Pédrot
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-05-26Update infer_conv to record trivial Prop <= Type i constraints that are neede...Matthieu Sozeau
2014-05-08Fast-path equality of sorts in compare_constr*Matthieu Sozeau
2014-05-06Add missing case for primitive projection in fold_map.Matthieu Sozeau
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06Cleanup 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-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-28Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toHugo Herbelin
2014-04-24Adding a [fold_map] operation on constrs.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Removing generic hashes in kernel.Pierre-Marie Pédrot
2014-03-02Fixing generic Hashtbl.hash in Constr.Pierre-Marie Pédrot
2013-11-04Using allocation-free version of Array higher-order function in criticalppedrot
2013-10-27More sharing in Constr.map_with_binders.ppedrot
2013-10-24Specializing hash functions for widely used types.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:51:42 +0000