index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
univ.mli
Age
Commit message (
Expand
)
Author
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-07-25
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-06-06
ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...
soubiran
2008-05-12
Changement de stratégie vis à vis du commit 10859 sur la gestion des
herbelin
2008-04-27
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-21
added the .vo checker (with independent Makefile)
barras
2007-12-18
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-09-30
Ajout infos de débogage de "universe inconsistency" quand option Set
herbelin
2007-05-11
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-01-19
Prise en compte des univers algébriques dans les types inférés dans
herbelin
2006-05-23
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-03-29
Inductifs avec polymorphisme de sorte (version initiale)
herbelin
2005-05-05
Code v7 obsolete
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2001-11-12
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-05
GROS COMMIT:
barras
2001-09-20
Nettoyage des commentaires
herbelin
2001-09-09
Passage aux univers algébriques
herbelin
2001-07-03
Ajout hashconsing univers
herbelin
2001-05-29
Facilites pour le debogguage des univers.
coq
2001-03-28
amelioration de la structure des univers
barras
2001-03-15
entetes
filliatr
2000-12-12
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-11-28
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-10-06
MAJ pr_uni
herbelin
2000-10-06
correction bug univers (dummy_univ)
filliatr
1999-09-25
ensembles de contraintes d'univers
filliatr
1999-09-03
modules Libobject et Summary (partiel)
filliatr
1999-08-30
un petit effort de presentation dans les interfaces
filliatr
1999-08-26
- abstraction
filliatr
1999-08-24
mach et himsg; typage sans extraction
filliatr
1999-08-20
machine: execute = typage avec univers
filliatr
1999-08-18
module Reduction (fin)
filliatr
1999-08-18
module Reduction (debut)
filliatr
1999-08-17
generic, term et evd
filliatr