aboutsummaryrefslogtreecommitdiff
path: root/contrib/ring
AgeCommit message (Collapse)Author
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
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@4051 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Notations arithmetiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4008 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Alignement du comportement des implicites d'inductif en sortie de section ↵herbelin
sur celui des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3880 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Remplacement Grammar par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3357 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3355 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-28Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3317 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-26Remplacement des Grammar et des [| |] par des notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3304 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-24Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3262 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-19Reparation de ring pour les setoidesclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2797 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2745 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
(did not return an ordered list of monomials). - improved unary negation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2692 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2651 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-05Suppression de l'application de f_equal2 pour "mult" (non inversible);herbelin
Application de f_equal2 pour "plus" seulement si soit les membres droits soit les membres gauches sont égaux. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2616 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-14reparation semi setoid ringclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2531 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 00:50:15 +0000