aboutsummaryrefslogtreecommitdiff
path: root/library/universes.mli
AgeCommit message (Expand)Author
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2016-10-20Cleanup code according to comments.Matthieu Sozeau
2016-10-20Fix minimization to be insensitive to redundant arcs.Matthieu Sozeau
2016-06-13Univs: more robust Universe/Constraint decls #4816Matthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-11-26More efficient implementation of equality-up-to-universes in Universes.Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-08Univs: fix bug #3807Matthieu Sozeau
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-21Cleanup substitution inside universe instances, only done through subst_fn now,Matthieu Sozeau
2014-07-03Cleanup code related to the constraint solving, which sits now outside theMatthieu Sozeau
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-10- Fix substitution of universes which needlessly hashconsed existing universes.Matthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-04- Fix hashing of levels to get the "right" order in universe contexts etc...Matthieu Sozeau
2014-05-06- Add back some compatibility functions to avoid rewriting plugins.Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06- Fix abstract forgetting about new constraints.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 08:51:12 +0000