aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring/quote.ml
Commit message (Expand)AuthorAge
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Protection des tactiques contre l'utilisation sans le bon contexte de thoriesGravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Nouveau Rewrite-in plus economiqueGravatar barras2002-03-04
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* ParsingGravatar herbelin2001-08-10
* Changement de la structure des points fixesGravatar barras2001-05-03
* réparation QuoteGravatar filliatr2001-04-09
* correction d'un bug de QuoteGravatar filliatr2001-04-06
* 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
* Now Ring does not perform any more the same reduction twice.Gravatar sacerdot2001-01-12
* Nouveau long long avec Coq en têteGravatar herbelin2000-11-29
* Prise en compte du repertoire dans le section path; utilisation de dirpath po...Gravatar herbelin2000-11-28
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* Simplification de l'accès aux globauxGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Renommage AppL en AppGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* *) -> i*)Gravatar filliatr2000-07-21
* RingGravatar filliatr2000-06-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 12:40:20 +0000