aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)Gravatar herbelin2010-04-20
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)Gravatar letouzey2008-11-16
* Correct display of constraints for Print Universes "dumpfile"Gravatar letouzey2008-11-15
* Faster comparison of universesGravatar letouzey2008-11-14
* 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
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* 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
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Simplification message d'anomalieGravatar herbelin2005-09-08
* Bug affichage graphe universGravatar herbelin2005-05-05
* MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...Gravatar herbelin2005-05-05
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)Gravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Passage aux univers algébriquesGravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* Ajout hashconsing universGravatar herbelin2001-07-03
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
* Changement de la structure des points fixesGravatar barras2001-05-03
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* ensembles de contraintes d'universGravatar filliatr1999-09-25
* - abstractionGravatar filliatr1999-08-26