aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring/quote.ml
AgeCommit message (Expand)Author
2002-03-04Nouveau Rewrite-in plus economiquebarras
2001-11-05GROS COMMIT:barras
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-08-10Parsingherbelin
2001-05-03Changement de la structure des points fixesbarras
2001-04-09réparation Quotefilliatr
2001-04-06correction d'un bug de Quotefilliatr
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
2001-01-12Now Ring does not perform any more the same reduction twice.sacerdot
2000-11-29Nouveau long long avec Coq en têteherbelin
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath po...herbelin
2000-11-26Appel des constantes globaux par des noms absolusherbelin
2000-11-23Simplification de l'accès aux globauxherbelin
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-20Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...herbelin
2000-10-01Renommage AppL en Appherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-07-21*) -> i*)filliatr
2000-06-21Ringfilliatr