aboutsummaryrefslogtreecommitdiff
path: root/parsing/coqlib.ml
AgeCommit message (Expand)Author
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-08-02Modules dans COQ\!\!\!\!coq
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