aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring/quote.ml
AgeCommit message (Expand)Author
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