aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
Commit message (Expand)AuthorAge
...
* 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
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Remove unused function in univGravatar Matthieu Sozeau2014-06-10
* Function in Univ uselessly exported.Gravatar Pierre-Marie Pédrot2014-06-08
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.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
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
* A version of Univ.check_eq with no anomaly for Evd.set_eq_sortGravatar letouzey2013-03-12
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
* Updating headers.Gravatar herbelin2012-08-08
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Fix the hconsing of universesGravatar letouzey2011-09-07
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* More coherent comment orderingGravatar glondu2011-01-11
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
* More generic Univ.dump_universesGravatar glondu2010-11-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...Gravatar soubiran2008-06-06
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 18:10:07 +0000