aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
Commit message (Expand)AuthorAge
* 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