aboutsummaryrefslogtreecommitdiff
path: root/parsing/coqlib.ml
AgeCommit message (Expand)Author
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-05GROS COMMIT:barras
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-08-10Parsingherbelin
2001-07-02Ajout glob_eq{,T}herbelin
2001-03-30branchement extraction (bytecode seulement)filliatr
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...herbelin