aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/coqlib.ml
Commit message (Expand)AuthorAge
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression de Logic_Type.sigT, redondant avec Specif.sigTGravatar herbelin2001-10-24
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* ParsingGravatar herbelin2001-08-10
* Ajout glob_eq{,T}Gravatar herbelin2001-07-02
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14