aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
Commit message (Expand)AuthorAge
...
* 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
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Code v7 obsoleteGravatar herbelin2005-05-05
* Nouvelle en-têteGravatar herbelin2004-07-16
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Nettoyage des commentairesGravatar herbelin2001-09-20
* Passage aux univers algébriquesGravatar herbelin2001-09-09
* Ajout hashconsing universGravatar herbelin2001-07-03
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* MAJ pr_uniGravatar herbelin2000-10-06
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* ensembles de contraintes d'universGravatar filliatr1999-09-25
* modules Libobject et Summary (partiel)Gravatar filliatr1999-09-03
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
* - abstractionGravatar filliatr1999-08-26
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
* machine: execute = typage avec universGravatar filliatr1999-08-20
* module Reduction (fin)Gravatar filliatr1999-08-18