aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.mli
AgeCommit message (Expand)Author
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06- Fix handling of polymorphic inductive elimination schemes.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-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-08-08Updating headers.herbelin
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
2011-10-10Hash-consing of mutual_inductive_body (and Univ.constraints)letouzey
2011-10-02Hash-consing of constr could share moreletouzey
2011-09-07Fix the hconsing of universesletouzey
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-01-11Add "Print Sorted Universes"glondu
2011-01-11More coherent comment orderingglondu
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-11-03In Univ, unify order_request and constraint_typeglondu
2010-11-02More generic Univ.dump_universesglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...soubiran
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-21added the .vo checker (with independent Makefile)barras
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-01-19Prise en compte des univers algébriques dans les types inférés dansherbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2005-05-05Code v7 obsoleteherbelin
2004-07-16Nouvelle en-têteherbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-09-20Nettoyage des commentairesherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-07-03Ajout hashconsing universherbelin
2001-05-29Facilites pour le debogguage des univers.coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 20:04:50 +0000