aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/universes.ml
Commit message (Expand)AuthorAge
* Optimizing the universes_of_constr_function.Gravatar Pierre-Marie Pédrot2016-02-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Univs: fix bug #4443.Gravatar Matthieu Sozeau2015-12-03
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Avoid recording spurious Set <= Top.i constraints which are alwaysGravatar Matthieu Sozeau2015-11-27
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: fix minimization to allow lowering a universe to Set, not Prop.Gravatar Matthieu Sozeau2015-10-02
* Univs: minimization, adapt to graph invariants.Gravatar Matthieu Sozeau2015-10-02
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Univs/minimization: Fix unused variable bug.Gravatar Matthieu Sozeau2015-07-07
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Fix bug #3446.Gravatar Matthieu Sozeau2015-06-11
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Strengthen minimization: it shouldn't set a universe u to a max if itGravatar Matthieu Sozeau2015-04-09
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.Gravatar Pierre-Marie Pédrot2014-11-10
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Fix computation of dangling constraints at the end of a proof (bug #3531).Gravatar Matthieu Sozeau2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Small code simplification.Gravatar Pierre-Marie Pédrot2014-08-05
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* More straightforward definition of Universes.add_list_map.Gravatar Pierre-Marie Pédrot2014-07-21
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Fixed some HoTT bugs, provide a proper error message when giving an ill-formedGravatar Matthieu Sozeau2014-06-20
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Function in Univ uselessly exported.Gravatar Pierre-Marie Pédrot2014-06-08
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
* Avoid u+k <= v constraints, don't take the sup of an algebraic universe duringGravatar Matthieu Sozeau2014-05-06
* - Add back some compatibility functions to avoid rewriting plugins.Gravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context to not remove useful constraints.Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 05:44:10 +0000