aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring
AgeCommit message (Collapse)Author
2001-07-10Setoid_rewrite -> Rewriteclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1847 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout des fichiers pour le Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1844 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-10Ajout d'un Ring pour setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1839 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-02Nettoyage/restructuration des ensembles d'indicateurs de réductionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1819 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-28patch Claudiofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1766 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-14réparation Ring (simplifications)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1750 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-09réparation Quotefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1559 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-06correction d'un bug de Quotefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1553 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01De bizarres SR_pus_assoc au lieu de SR_plus_assocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1421 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib ↵herbelin
(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1386 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib ↵herbelin
(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1380 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05rétablissement patch Claudiofilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1319 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-02retablissement (provisoire) de l'ancien Ring a cause d'une explosion en ↵filliatr
temps sur les preuves de Nijmegen + correction partielle de la simplification par Ring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1312 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-12Now Ring does not perform any more the same reduction twice.sacerdot
This was a logical bug of the sort_subterm function, in the sense that the aim of the function (as stated in the comment) was not to make early reductions mess with subterms; what happened, though, was that the first reduction completely removed the term and the second reduction became completely dummy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1247 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-12Comment fixedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Now reduction to normal form is done only when the term is notsacerdot
in normal form. Moreover refl_eq is no more used. Instead I use sym_eqT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1244 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Many unuseful rewritings are no more done by Ring.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1243 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Meta Definition -> Tactic Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1238 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-09Tactic Definition -> Meta Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1237 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Nouveau long long avec Coq en têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1020 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath ↵herbelin
pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Appel des constantes globaux par des noms absolusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@966 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon ↵filliatr
Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Simplification de l'accès aux globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@933 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵herbelin
'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21implicites manuelsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Remplacement des hacks pour les noms longs par un appel à ↵herbelin
Declare.global_qualified_reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@871 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15methode exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵herbelin
library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Correction sur commit errone de la version 1.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@815 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@814 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Semi_Ring_Theory_of decommentemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-26Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@765 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-25Manquait le cas Constr de dyn_polynomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@761 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Syntaxe des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@752 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-24Renommage command -> constr et changement des analyseurs syntaxiques de ↵herbelin
Grammar et Syntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@751 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23Modifications pour implicites améliorésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@746 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJ pour nouvelle syntaxe des membres droits des grammairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@672 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@635 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Abstraction de constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:34:53 +0000