aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring
AgeCommit message (Collapse)Author
2006-11-13Encore des _sym au lieu de _commherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9370 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26petits pbs de dependancesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9181 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26Compilation newringnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9180 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26commit de field + renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-06Nettoyage et documentation de Libraryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Implemented a test for "Add [Semi] Setoid Ring" to check that the givensacerdot
compatibility proofs are the default compatibility proofs for their respective operation. This closes a bug reported by Pierre Letouzey on coqdev. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6668 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||"sacerdot
prevendent detection of only one mistake in the user input. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6667 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02The statement of the compatibility theorem for addition and multiplicationsacerdot
have been changed to match the new statement used by Add Setoid. NOTE: this reveals a missing check in the code. Indeed, "Add Setoid Ring" does not check if the provided compatibility theorems have the expected type. To be done in a future commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6662 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02 setoid_rewrite t; [tac]sacerdot
now used in place of setoid_replace ... with ... ; try (exact t) ; tac The new stricter version closes a bug reported by Pierre Letouzey on coqdev. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6661 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-01The "Add Setoid" command now has a new argument "as name" that is usedsacerdot
to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
Thus it does not work for setoid relations and it can replace setoid_replace when the user wants to specify what the relation should be. To solve the problem this commit enables the syntax setoid_replace E1 with E2 using relation R ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29New syntaxsacerdot
"setoid_rewrite dir term generate side conditions constr_list" to specify a list of side conditions that must be a subset of the generated new goals. Used to disambiguate in case of multiple set of generated side conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03Ported to the new implementation of setoid_*.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6050 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03The old implementation of (setoid_replace c1 with c2) used to replacesacerdot
either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation will not do it. Thus I am replacing every occurrence of (setoid_replace c1 with c2) with (setoid_replace c1 with c2 || setoid_replace c2 with c1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6047 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23Setoid_replace.setoid_replace: last argument (that was supposed to besacerdot
always None) removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5969 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-22correction d'un bug de la tactique pour les semi setoid rings.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5965 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25eq and eqT are the samebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Ordre standard pour l'associativiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4908 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Noms/énoncés plus canoniquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres ↵herbelin
positifs et naturels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4810 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵herbelin
associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout notations pour les expressions dans un anneauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4735 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Simplification preuveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4734 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Ajout NArithRingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4703 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-06distinguer interp_cs et interp_setcsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4529 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-03Cacher les .v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-28oupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4497 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-282 pbs de plus réglés concernant Setoid Ring:letouzey
- pf_conv_x parfois utilisé sur des termes non typés -> un try with - setoid_replace peut parfois résoudre seul l'égalité utilisé -> un tclTRY git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4496 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Un peu plus de souplesse dans la globalisation des noms utilises par les ↵herbelin
tactiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22commit accidentel d'une bidouilleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4451 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22suite (et fin) reparation Setoid Ringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4444 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22tentative de rafraichissement de Setoid Ringletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4439 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4433 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notations ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4053 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4052 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 16:48:37 +0000