index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
univ.mli
Commit message (
Expand
)
Author
Age
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
GROS COMMIT:
barras
2001-11-05
*
Nettoyage des commentaires
herbelin
2001-09-20
*
Passage aux univers algébriques
herbelin
2001-09-09
*
Ajout hashconsing univers
herbelin
2001-07-03
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
MAJ pr_uni
herbelin
2000-10-06
*
correction bug univers (dummy_univ)
filliatr
2000-10-06
*
ensembles de contraintes d'univers
filliatr
1999-09-25
*
modules Libobject et Summary (partiel)
filliatr
1999-09-03
*
un petit effort de presentation dans les interfaces
filliatr
1999-08-30
*
- abstraction
filliatr
1999-08-26
*
mach et himsg; typage sans extraction
filliatr
1999-08-24
*
machine: execute = typage avec univers
filliatr
1999-08-20
*
module Reduction (fin)
filliatr
1999-08-18
*
module Reduction (debut)
filliatr
1999-08-18
*
generic, term et evd
filliatr
1999-08-17