aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring
Commit message (Expand)AuthorAge
* Modification de l'emplacement des fichiers pour les setoides.Gravatar clrenard2001-09-18
* MAJ vis à vis de la nouvelle non-localité des Remark/FactGravatar herbelin2001-09-14
* ParsingGravatar herbelin2001-08-10
* Passage au nouveau DestructGravatar herbelin2001-08-07
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* Setoid_rewrite -> RewriteGravatar clrenard2001-07-10
* Ajout des fichiers pour le Ring pour setoidesGravatar clrenard2001-07-10
* Ajout d'un Ring pour setoidesGravatar clrenard2001-07-10
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* patch ClaudioGravatar filliatr2001-05-28
* réparation Ring (simplifications)Gravatar filliatr2001-05-14
* 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
* De bizarres SR_pus_assoc au lieu de SR_plus_assocGravatar herbelin2001-03-01
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Renommage des variables dans les schémas d'inductionGravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* rétablissement patch ClaudioGravatar filliatr2001-02-05
* retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...Gravatar filliatr2001-02-02
* - coqc : option -imageGravatar filliatr2001-02-01
* Now Ring does not perform any more the same reduction twice.Gravatar sacerdot2001-01-12
* Comment fixedGravatar sacerdot2001-01-12
* Now reduction to normal form is done only when the term is notGravatar sacerdot2001-01-11
* Many unuseful rewritings are no more done by Ring.Gravatar sacerdot2001-01-11
* Meta Definition -> Tactic DefinitionGravatar delahaye2001-01-09
* Tactic Definition -> Meta DefinitionGravatar delahaye2001-01-09
* 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
* Elimination du 'Gravatar delahaye2000-11-28
* Appel des constantes globaux par des noms absolusGravatar herbelin2000-11-26
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* 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
* implicites manuelsGravatar filliatr2000-11-21
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Correction sur commit errone de la version 1.3Gravatar herbelin2000-11-07
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
* Semi_Ring_Theory_of decommenteGravatar mohring2000-10-26
* Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'Gravatar herbelin2000-10-26
* Manquait le cas Constr de dyn_polynomGravatar herbelin2000-10-25
* Syntaxe des tactiquesGravatar herbelin2000-10-24
* Renommage command -> constr et changement des analyseurs syntaxiques de Gramm...Gravatar herbelin2000-10-24
* Modifications pour implicites améliorésGravatar herbelin2000-10-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 08:44:24 +0000