From 4dc282b8b71479d45704b414d1a10a27e71752f1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 4 Sep 2008 22:28:14 +0000 Subject: [PATCH] transcript: improved debuugging facilities orocedural/Coq: we escaped the non-ASCII7 characters --- .../components/binaries/transcript/.depend | 16 +- .../binaries/transcript/.depend.opt | 16 +- .../components/binaries/transcript/Makefile | 2 +- .../components/binaries/transcript/grafite.ml | 21 +- .../components/binaries/transcript/options.ml | 32 ++ .../components/binaries/transcript/top.ml | 8 +- .../binaries/transcript/v8Lexer.mll | 16 +- .../binaries/transcript/v8Parser.mly | 5 +- .../contribs/procedural/Coq/Bool/Bvector.mma | 46 +- .../Coq/Logic/ClassicalDescription.mma | 2 +- .../contribs/procedural/Coq/Logic/Eqdep.mma | 2 +- .../contribs/procedural/Coq/NArith/BinPos.mma | 2 +- .../contribs/procedural/Coq/NArith/Pnat.mma | 2 +- .../procedural/Coq/Reals/RiemannInt.mma | 2 +- .../contribs/procedural/Coq/Reals/Rprod.mma | 2 +- .../contribs/procedural/Coq/ZArith/BinInt.mma | 2 +- .../contribs/procedural/Coq/ZArith/Zabs.mma | 2 +- .../procedural/Coq/ZArith/Zbinary.mma | 28 +- .../procedural/Coq/ZArith/Zcompare.mma | 2 +- .../contribs/procedural/Coq/ZArith/Zdiv.mma | 2 +- .../contribs/procedural/Coq/ZArith/Zmin.mma | 2 +- .../contribs/procedural/Coq/ZArith/Znat.mma | 2 +- .../contribs/procedural/Coq/ZArith/Zorder.mma | 2 +- .../procedural/Coq/ZArith/auxiliary.mma | 2 +- .../matita/contribs/procedural/Coq/depends | 451 ++++++++++++++++++ .../contribs/procedural/Makefile.common | 8 +- 26 files changed, 592 insertions(+), 85 deletions(-) create mode 100644 helm/software/components/binaries/transcript/options.ml create mode 100644 helm/software/matita/contribs/procedural/Coq/depends diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 5e737a14a..793da9940 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,12 +1,12 @@ v8Parser.cmi: types.cmo grafite.cmi: types.cmo -v8Parser.cmo: types.cmo v8Parser.cmi -v8Parser.cmx: types.cmx v8Parser.cmi -v8Lexer.cmo: v8Parser.cmi -v8Lexer.cmx: v8Parser.cmx -grafite.cmo: types.cmo grafite.cmi -grafite.cmx: types.cmx grafite.cmi +v8Parser.cmo: types.cmo options.cmo v8Parser.cmi +v8Parser.cmx: types.cmx options.cmx v8Parser.cmi +v8Lexer.cmo: v8Parser.cmi options.cmo +v8Lexer.cmx: v8Parser.cmx options.cmx +grafite.cmo: types.cmo options.cmo grafite.cmi +grafite.cmx: types.cmx options.cmx grafite.cmi engine.cmo: v8Parser.cmi v8Lexer.cmo types.cmo grafite.cmi engine.cmi engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi -top.cmo: engine.cmi -top.cmx: engine.cmx +top.cmo: options.cmo engine.cmi +top.cmx: options.cmx engine.cmx diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index 61ce486f9..01bfffa30 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,12 +1,12 @@ v8Parser.cmi: types.cmx grafite.cmi: types.cmx -v8Parser.cmo: types.cmx v8Parser.cmi -v8Parser.cmx: types.cmx v8Parser.cmi -v8Lexer.cmo: v8Parser.cmi -v8Lexer.cmx: v8Parser.cmx -grafite.cmo: types.cmx grafite.cmi -grafite.cmx: types.cmx grafite.cmi +v8Parser.cmo: types.cmx options.cmx v8Parser.cmi +v8Parser.cmx: types.cmx options.cmx v8Parser.cmi +v8Lexer.cmo: v8Parser.cmi options.cmx +v8Lexer.cmx: v8Parser.cmx options.cmx +grafite.cmo: types.cmx options.cmx grafite.cmi +grafite.cmx: types.cmx options.cmx grafite.cmi engine.cmo: v8Parser.cmi v8Lexer.cmx types.cmx grafite.cmi engine.cmi engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi -top.cmo: engine.cmi -top.cmx: engine.cmx +top.cmo: options.cmx engine.cmi +top.cmx: options.cmx engine.cmx diff --git a/helm/software/components/binaries/transcript/Makefile b/helm/software/components/binaries/transcript/Makefile index b9bfc6109..4bcb2d53f 100644 --- a/helm/software/components/binaries/transcript/Makefile +++ b/helm/software/components/binaries/transcript/Makefile @@ -4,7 +4,7 @@ H=@ REQUIRES = unix str helm-grafite_parser -MLS = types.ml v8Parser.ml v8Lexer.ml grafite.ml engine.ml top.ml +MLS = types.ml options.ml v8Parser.ml v8Lexer.ml grafite.ml engine.ml top.ml MLIS = v8Parser.mli grafite.mli engine.mli CLEAN = v8Parser.ml v8Parser.mli v8Lexer.ml diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 1f9b36866..f5c4a49f8 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -24,6 +24,7 @@ *) module T = Types +module O = Options module UM = UriManager module NP = CicNotationPp @@ -93,20 +94,26 @@ let commit kind och items = let trd_rth kind (_, _, x, y, z) = kind, x, y, z in let commit = function | T.Heading heading -> out_preamble och heading - | T.Line line -> out_line_comment och line + | T.Line line -> + if !O.comments then out_line_comment och line | T.Include script -> out_command och (require script) - | T.Coercion specs -> out_unexported och "COERCION" (snd specs) - | T.Notation specs -> out_unexported och "NOTATION" (snd specs) (**) + | T.Coercion specs -> + if !O.comments then out_unexported och "COERCION" (snd specs) + | T.Notation specs -> + if !O.comments then out_unexported och "NOTATION" (snd specs) (**) | T.Inline (_, T.Var, src, _, _) -> - out_unexported och "UNEXPORTED" src + if !O.comments then out_unexported och "UNEXPORTED" src (* FG: we do not export variables because we cook the other object * let name = UriManager.name_of_uri (UriManager.uri_of_string src) in * out_alias och name src *) | T.Inline specs -> out_command och (inline (trd_rth kind specs)) - | T.Section specs -> out_unexported och "UNEXPORTED" (trd specs) - | T.Comment comment -> out_comment och comment - | T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport + | T.Section specs -> + if !O.comments then out_unexported och "UNEXPORTED" (trd specs) + | T.Comment comment -> + if !O.comments then out_comment och comment + | T.Unexport unexport -> + if !O.comments then out_unexported och "UNEXPORTED" unexport | T.Verbatim verbatim -> out_verbatim och verbatim | T.Discard _ -> () in diff --git a/helm/software/components/binaries/transcript/options.ml b/helm/software/components/binaries/transcript/options.ml new file mode 100644 index 000000000..e259494b0 --- /dev/null +++ b/helm/software/components/binaries/transcript/options.ml @@ -0,0 +1,32 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let verbose_parser = ref false + +let verbose_lexer = ref false + +let verbose_escape = ref false + +let comments = ref true diff --git a/helm/software/components/binaries/transcript/top.ml b/helm/software/components/binaries/transcript/top.ml index 5ef75dab7..5b3b23473 100644 --- a/helm/software/components/binaries/transcript/top.ml +++ b/helm/software/components/binaries/transcript/top.ml @@ -27,9 +27,15 @@ let main = let cwd = ref Filename.current_dir_name in let help = "Usage: transcript [ -C ] [ | ]*" in let help_C = " set working directory to " in + let help_vp = " verbose parsing" in + let help_vl = " verbose lexing" in + let help_vx = " verbose character escaping" in let set_cwd dir = cwd := dir in let process_package package = Engine.produce (Engine.make !cwd package) in Engine.init (); Arg.parse [ - ("-C", Arg.String set_cwd, help_C) + ("-C", Arg.String set_cwd, help_C); + ("-vp", Arg.Set Options.verbose_parser, help_vp); + ("-vl", Arg.Set Options.verbose_lexer, help_vl); + ("-vx", Arg.Set Options.verbose_escape, help_vx); ] process_package help diff --git a/helm/software/components/binaries/transcript/v8Lexer.mll b/helm/software/components/binaries/transcript/v8Lexer.mll index 57f7d16ae..0ef38a919 100644 --- a/helm/software/components/binaries/transcript/v8Lexer.mll +++ b/helm/software/components/binaries/transcript/v8Lexer.mll @@ -1,7 +1,17 @@ { + module O = Options module P = V8Parser - let out t s = prerr_endline (t ^ " " ^ s) + let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) + + let check s = + let c = Char.code s.[0] in + if c <= 127 then s else + let escaped = Printf.sprintf "\\%3u\\" c in + begin + if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped; + escaped + end } let QT = '"' @@ -89,6 +99,6 @@ rule token = parse | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s } | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s } | "," { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s } - | ".." { let s = Lexing.lexeme lexbuf in out "SPEC" s; P.EXTRA s } - | _ { let s = Lexing.lexeme lexbuf in out "SPEC" s; P.EXTRA s } + | _ + { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s } | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly index 52456c559..4627cf9a2 100644 --- a/helm/software/components/binaries/transcript/v8Parser.mly +++ b/helm/software/components/binaries/transcript/v8Parser.mly @@ -25,8 +25,9 @@ %{ module T = Types - - let out t s = prerr_endline ("-- " ^ t ^ " " ^ s) + module O = Options + + let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s) let trim = HExtlib.trim_blanks diff --git a/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma b/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma index 0894e8eea..c50415fec 100644 --- a/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma +++ b/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma @@ -46,17 +46,17 @@ Open Local Scope nat_scope. (* On s'inspire de PolyList pour fabriquer les vecteurs de bits. -La dimension du vecteur est un paramètre trop important pour +La dimension du vecteur est un param\232\tre trop important pour se contenter de la fonction "length". -La première idée est de faire un record avec la liste et la longueur. +La premi\232\re id\233\e est de faire un record avec la liste et la longueur. Malheureusement, cette verification a posteriori amene a faire de nombreux lemmes pour gerer les longueurs. -La seconde idée est de faire un type dépendant dans lequel la -longueur est un paramètre de construction. Cela complique un -peu les inductions structurelles, la solution qui a ma préférence -est alors d'utiliser un terme de preuve comme définition. +La seconde id\233\e est de faire un type d\233\pendant dans lequel la +longueur est un param\232\tre de construction. Cela complique un +peu les inductions structurelles, la solution qui a ma pr\233\f\233\rence +est alors d'utiliser un terme de preuve comme d\233\finition. -(En effet une définition comme : +(En effet une d\233\finition comme : Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) := Cases v of | Vnil => Vnil @@ -97,16 +97,16 @@ Section VECTORS *) (* -Un vecteur est une liste de taille n d'éléments d'un ensemble A. -Si la taille est non nulle, on peut extraire la première composante et -le reste du vecteur, la dernière composante ou rajouter ou enlever -une composante (carry) ou repeter la dernière composante en fin de vecteur. -On peut aussi tronquer le vecteur de ses p dernières composantes ou -au contraire l'étendre (concaténer) d'un vecteur de longueur p. -Une fonction unaire sur A génère une fonction des vecteurs de taille n -dans les vecteurs de taille n en appliquant f terme à terme. -Une fonction binaire sur A génère une fonction des couple de vecteurs -de taille n dans les vecteurs de taille n en appliquant f terme à terme. +Un vecteur est une liste de taille n d'\233\l\233\ments d'un ensemble A. +Si la taille est non nulle, on peut extraire la premi\232\re composante et +le reste du vecteur, la derni\232\re composante ou rajouter ou enlever +une composante (carry) ou repeter la derni\232\re composante en fin de vecteur. +On peut aussi tronquer le vecteur de ses p derni\232\res composantes ou +au contraire l'\233\tendre (concat\233\ner) d'un vecteur de longueur p. +Une fonction unaire sur A g\233\n\232\re une fonction des vecteurs de taille n +dans les vecteurs de taille n en appliquant f terme \224\ terme. +Une fonction binaire sur A g\233\n\232\re une fonction des couple de vecteurs +de taille n dans les vecteurs de taille n en appliquant f terme \224\ terme. *) (* UNEXPORTED @@ -166,14 +166,14 @@ Section BOOLEAN_VECTORS *) (* -Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. -ATTENTION : le stockage s'effectue poids FAIBLE en tête. +Un vecteur de bits est un vecteur sur l'ensemble des bool\233\ens de longueur fixe. +ATTENTION : le stockage s'effectue poids FAIBLE en t\234\te. On en extrait le bit de poids faible (head) et la fin du vecteur (tail). -On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs. -On calcule les décalages d'une position vers la gauche (vers les poids forts, on +On calcule la n\233\gation d'un vecteur, le et, le ou et le xor bit \224\ bit de 2 vecteurs. +On calcule les d\233\calages d'une position vers la gauche (vers les poids forts, on utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en -insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique). -ATTENTION : Tous les décalages prennent la taille moins un comme paramètre +ins\233\rant un bit 'carry' (logique) ou en r\233\p\233\tant le bit de poids fort (arithm\233\tique). +ATTENTION : Tous les d\233\calages prennent la taille moins un comme param\232\tre (ils ne travaillent que sur des vecteurs au moins de longueur un). *) diff --git a/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma b/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma index 7ab50d014..82db6eb1f 100644 --- a/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma +++ b/helm/software/matita/contribs/procedural/Coq/Logic/ClassicalDescription.mma @@ -39,7 +39,7 @@ include "Coq.ma". implies a strongly classical world. Especially it conflicts with impredicativity of Set, knowing that true<>false in Set. - [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical + [1] Laurent Chicli, Lo\239\c Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) diff --git a/helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma b/helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma index 4efee3045..283a2fd5b 100644 --- a/helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma +++ b/helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.mma @@ -48,7 +48,7 @@ include "Coq.ma". References: [1] T. Streicher, Semantical Investigations into Intensional Type Theory, - Habilitationsschrift, LMU München, 1993. + Habilitationsschrift, LMU M\252\nchen, 1993. [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, Proceedings of the meeting Twenty-five years of constructive type theory, Venice, Oxford University Press, 1998 diff --git a/helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma b/helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma index 18782ade8..ac333d7c3 100644 --- a/helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma +++ b/helm/software/matita/contribs/procedural/Coq/NArith/BinPos.mma @@ -36,7 +36,7 @@ include "Coq.ma". (*#* Binary positive numbers *) -(*#* Original development by Pierre Crégut, CNET, Lannion, France *) +(*#* Original development by Pierre Cr\233\gut, CNET, Lannion, France *) inline procedural "cic:/Coq/NArith/BinPos/positive.ind". diff --git a/helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma b/helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma index da44e4188..2d835257e 100644 --- a/helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma +++ b/helm/software/matita/contribs/procedural/Coq/NArith/Pnat.mma @@ -39,7 +39,7 @@ include "NArith/BinPos.ma". (*#* Properties of the injection from binary positive numbers to Peano natural numbers *) -(*#* Original development by Pierre Crégut, CNET, Lannion, France *) +(*#* Original development by Pierre Cr\233\gut, CNET, Lannion, France *) include "Arith/Le.ma". diff --git a/helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma b/helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma index d4704676b..b032806c8 100644 --- a/helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma +++ b/helm/software/matita/contribs/procedural/Coq/Reals/RiemannInt.mma @@ -92,7 +92,7 @@ inline procedural "cic:/Coq/Reals/RiemannInt/RiemannInt_P5.con" as lemma. (*#*************************************) -(* C°([a,b]) is included in L1([a,b]) *) +(* C\176\([a,b]) is included in L1([a,b]) *) (*#*************************************) diff --git a/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma b/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma index b85e45590..db3a0a34e 100644 --- a/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma +++ b/helm/software/matita/contribs/procedural/Coq/Reals/Rprod.mma @@ -70,7 +70,7 @@ inline procedural "cic:/Coq/Reals/Rprod/fact_prodSO.con" as lemma. inline procedural "cic:/Coq/Reals/Rprod/le_n_2n.con" as lemma. -(* We prove that (N!)²<=(2N-k)!*k! forall k in [|O;2N|] *) +(* We prove that (N!)\178\<=(2N-k)!*k! forall k in [|O;2N|] *) inline procedural "cic:/Coq/Reals/Rprod/RfactN_fact2N_factk.con" as lemma. diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma index 34bd26086..b773d2163 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/BinInt.mma @@ -34,7 +34,7 @@ include "Coq.ma". (*#**********************************************************) -(*#* Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *) (*#**********************************************************) diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma index 32f52201e..c1a764ae9 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zabs.mma @@ -32,7 +32,7 @@ include "Coq.ma". (*i $Id: Zabs.v,v 1.4 2003/11/29 17:28:45 herbelin Exp $ i*) -(*#* Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *) include "Arith/Arith.ma". diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma index a1c27a484..87df305f6 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zbinary.mma @@ -42,10 +42,10 @@ include "ZArith/ZArith.ma". include "ZArith/Zpower.ma". (* -L'évaluation des vecteurs de booléens se font à la fois en binaire et -en complément à deux. Le nombre appartient à Z. +L'\195\\169\valuation des vecteurs de bool\195\\169\ens se font \195\\160\ la fois en binaire et +en compl\195\\169\ment \195\\160\ deux. Le nombre appartient \195\\160\ Z. On utilise donc Omega pour faire les calculs dans Z. -De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur. +De plus, on utilise les fonctions 2^n o\195\\185\ n est un naturel, ici la longueur. two_power_nat = [n:nat](POS (shift_nat n xH)) : nat->Z two_power_nat_S @@ -59,12 +59,12 @@ Section VALUE_OF_BOOLEAN_VECTORS *) (* -Les calculs sont effectués dans la convention positive usuelle. -Les valeurs correspondent soit à l'écriture binaire (nat), -soit au complément à deux (int). -On effectue le calcul suivant le schéma de Horner. -Le complément à deux n'a de sens que sur les vecteurs de taille -supérieure ou égale à un, le bit de signe étant évalué négativement. +Les calculs sont effectu\195\\169\s dans la convention positive usuelle. +Les valeurs correspondent soit \195\\160\ l'\195\\169\criture binaire (nat), +soit au compl\195\\169\ment \195\\160\ deux (int). +On effectue le calcul suivant le sch\195\\169\ma de Horner. +Le compl\195\\169\ment \195\\160\ deux n'a de sens que sur les vecteurs de taille +sup\195\\169\rieure ou \195\\169\gale \195\\160\ un, le bit de signe \195\\169\tant \195\\169\valu\195\\169\ n\195\\169\gativement. *) inline procedural "cic:/Coq/ZArith/Zbinary/bit_value.con" as definition. @@ -95,11 +95,11 @@ Section ENCODING_VALUE (* On calcule la valeur binaire selon un schema de Horner. -Le calcul s'arrete à la longueur du vecteur sans vérification. +Le calcul s'arrete \195\\160\ la longueur du vecteur sans v\195\\169\rification. On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient de la division z=2q+r avec 0<=r<=1. -La valeur en complément à deux est calculée selon un schema de Horner -avec Zmod2, le paramètre est la taille moins un. +La valeur en compl\195\\169\ment \195\\160\ deux est calcul\195\\169\e selon un schema de Horner +avec Zmod2, le param\195\\168\tre est la taille moins un. *) inline procedural "cic:/Coq/ZArith/Zbinary/Zmod2.con" as definition. @@ -215,8 +215,8 @@ Section COHERENT_VALUE *) (* -On vérifie que dans l'intervalle de définition les fonctions sont -réciproques l'une de l'autre. +On v\195\\169\rifie que dans l'intervalle de d\195\\169\finition les fonctions sont +r\195\\169\ciproques l'une de l'autre. Elles utilisent les lemmes du bric-a-brac. *) diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma index 539d29adf..484ab7dd4 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zcompare.mma @@ -50,7 +50,7 @@ Open Local Scope Z_scope. (*#*********************************************************************) -(*#* Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *) (*#*********************************************************************) diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma index 570b0350d..37d8af215 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.mma @@ -32,7 +32,7 @@ include "Coq.ma". (*i $Id: Zdiv.v,v 1.21 2003/11/29 17:28:45 herbelin Exp $ i*) -(* Contribution by Claude Marché and Xavier Urbain *) +(* Contribution by Claude March\233\ and Xavier Urbain *) (*#* diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma index ab193ad2e..97df3d263 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zmin.mma @@ -32,7 +32,7 @@ include "Coq.ma". (*i $Id: Zmin.v,v 1.3 2003/11/29 17:28:45 herbelin Exp $ i*) -(*#* Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *) include "Arith/Arith.ma". diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma index 92a6310b8..2dca10d37 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Znat.mma @@ -32,7 +32,7 @@ include "Coq.ma". (*i $Id: Znat.v,v 1.3 2003/12/15 19:48:23 barras Exp $ i*) -(*#* Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *) include "Arith/Arith.ma". diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma index 1d274647a..cef5a51ac 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/Zorder.mma @@ -32,7 +32,7 @@ include "Coq.ma". (*i $Id: Zorder.v,v 1.6 2003/11/29 17:28:45 herbelin Exp $ i*) -(*#* Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut (CNET, Lannion, France) *) include "NArith/BinPos.ma". diff --git a/helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma b/helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma index 0eeec1311..5f6e88a08 100644 --- a/helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma +++ b/helm/software/matita/contribs/procedural/Coq/ZArith/auxiliary.mma @@ -32,7 +32,7 @@ include "Coq.ma". (*i $Id: auxiliary.v,v 1.12 2003/11/29 17:28:46 herbelin Exp $ i*) -(*#* Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *) include "Arith/Arith.ma". diff --git a/helm/software/matita/contribs/procedural/Coq/depends b/helm/software/matita/contribs/procedural/Coq/depends new file mode 100644 index 000000000..14c774443 --- /dev/null +++ b/helm/software/matita/contribs/procedural/Coq/depends @@ -0,0 +1,451 @@ +IntMap/Addec.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma +Reals/Rprod.mma Arith/Compare.ma Coq.ma Reals/Binomial.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma +Num/GtProps.ma Num/GtProps.mma +Arith/Peano_dec.mma Coq.ma Logic/Decidable.ma +Num/NeqAxioms.mma Coq.ma Num/EqParams.ma Num/NeqParams.ma +IntMap/Addr.ma IntMap/Addr.mma +Bool/Sumbool.ma Bool/Sumbool.mma +Reals/Raxioms.ma Reals/Raxioms.mma +Wellfounded/Lexicographic_Exponentiation.ma Wellfounded/Lexicographic_Exponentiation.mma +Num/GtAxioms.mma Coq.ma Num/Axioms.ma Num/LeProps.ma +Num/Nat/NeqDef.mma Coq.ma Num/Params.ma +ZArith/Zmin.mma Arith/Arith.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma +ZArith/auxiliary.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Peano_dec.ma Coq.ma Logic/Decidable.ma ZArith/BinInt.ma ZArith/Zorder.ma +Num/AddProps.mma Coq.ma Num/Axioms.ma Num/EqAxioms.ma +Reals/RiemannInt.ma Reals/RiemannInt.mma +Arith/Lt.mma Arith/Le.ma Coq.ma +Arith/Max.mma Arith/Arith.ma Coq.ma +Reals/Rtrigo_reg.mma Coq.ma Reals/PSeries_reg.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +Num/DiscrProps.ma Num/DiscrProps.mma +Sets/Partial_Order.ma Sets/Partial_Order.mma +Num/NeqDef.mma Coq.ma Num/EqAxioms.ma Num/EqParams.ma Num/Params.ma +Lists/ListSet.ma Lists/ListSet.mma +Wellfounded/Disjoint_Union.ma Wellfounded/Disjoint_Union.mma +Bool/Sumbool.mma Coq.ma +Init/Datatypes.ma Init/Datatypes.mma +Num/NeqParams.mma Coq.ma Num/Params.ma +Arith/Div2.mma Arith/Compare_dec.ma Arith/Even.ma Arith/Lt.ma Arith/Plus.ma Coq.ma +Reals/Rderiv.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rlimit.ma +ZArith/Zpower.ma ZArith/Zpower.mma +IntMap/Lsort.ma IntMap/Lsort.mma +IntMap/Mapc.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma +Reals/Rbase.mma Coq.ma Reals/DiscrR.ma Reals/RIneq.ma Reals/Raxioms.ma Reals/Rdefinitions.ma +IntMap/Allmaps.mma Coq.ma IntMap/Adalloc.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapc.ma IntMap/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapfold.ma IntMap/Mapiter.ma IntMap/Maplists.ma IntMap/Mapsubset.ma +Num/OppAxioms.mma Coq.ma +Wellfounded/Inclusion.ma Wellfounded/Inclusion.mma +Logic/Classical.ma Logic/Classical.mma +Relations/Relation_Definitions.mma Coq.ma +Sets/Cpo.mma Coq.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Relations_1.ma +Reals/Ranalysis1.ma Reals/Ranalysis1.mma +Logic/Classical.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma +ZArith/Zhints.mma Coq.ma ZArith/BinInt.ma ZArith/Wf_Z.ma ZArith/Zabs.ma ZArith/Zcompare.ma ZArith/Zmin.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma ZArith/auxiliary.ma +Reals/Rtopology.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/RList.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma +Logic/ClassicalFacts.ma Logic/ClassicalFacts.mma +Reals/ArithProp.ma Reals/ArithProp.mma +Relations/Newman.mma Coq.ma Relations/Rstar.ma +ZArith/Zorder.ma ZArith/Zorder.mma +Init/Peano.ma Init/Peano.mma +Wellfounded/Wellfounded.mma Coq.ma Wellfounded/Disjoint_Union.ma Wellfounded/Inclusion.ma Wellfounded/Inverse_Image.ma Wellfounded/Lexicographic_Exponentiation.ma Wellfounded/Lexicographic_Product.ma Wellfounded/Transitive_Closure.ma Wellfounded/Union.ma Wellfounded/Well_Ordering.ma +IntMap/Addr.mma Bool/Bool.ma Coq.ma ZArith/ZArith.ma +Num/LeProps.mma Coq.ma Num/LeAxioms.ma Num/LtProps.ma +Arith/Compare_dec.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Decidable.ma +Sets/Integers.mma Arith/Compare_dec.ma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Image.ma Sets/Infinite_sets.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma Sets/Relations_1.ma +Reals/DiscrR.mma Coq.ma Reals/RIneq.ma +IntMap/Fset.ma IntMap/Fset.mma +Reals/Integration.ma Reals/Integration.mma +Reals/Rtrigo_alt.ma Reals/Rtrigo_alt.mma +Init/Notations.ma Init/Notations.mma +NArith/BinNat.mma Coq.ma NArith/BinPos.ma +Reals/Ranalysis4.ma Reals/Ranalysis4.mma +Reals/Rseries.mma Arith/Compare.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma +Arith/Factorial.mma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma +Sets/Classical_sets.ma Sets/Classical_sets.mma +Reals/RList.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma +Reals/DiscrR.ma Reals/DiscrR.mma +Sets/Image.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma +Sets/Relations_1_facts.mma Coq.ma Sets/Relations_1.ma +Reals/Rtrigo_reg.ma Reals/Rtrigo_reg.mma +ZArith/ZArith.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zbool.ma ZArith/Zcomplements.ma ZArith/Zdiv.ma ZArith/Zlogarithm.ma ZArith/Zpower.ma ZArith/Zsqrt.ma +Sets/Powerset_Classical_facts.mma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Powerset_facts.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma +ZArith/Zlogarithm.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zpower.ma +Reals/Rtopology.ma Reals/Rtopology.mma +Reals/Rtrigo_fun.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma +Sets/Ensembles.ma Sets/Ensembles.mma +Reals/Rdefinitions.ma Reals/Rdefinitions.mma +Num/GtProps.mma Coq.ma +ZArith/Zmisc.ma ZArith/Zmisc.mma +Sets/Relations_1.ma Sets/Relations_1.mma +Reals/Alembert.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma +Sets/Powerset.ma Sets/Powerset.mma +ZArith/Zcompare.ma ZArith/Zcompare.mma +Sets/Finite_sets_facts.ma Sets/Finite_sets_facts.mma +Sets/Relations_3_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma Sets/Relations_2_facts.ma Sets/Relations_3.ma +Arith/Mult.ma Arith/Mult.mma +Wellfounded/Lexicographic_Exponentiation.mma Coq.ma Lists/List.ma Logic/Eqdep.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma +Logic/ChoiceFacts.ma Logic/ChoiceFacts.mma +Num/EqParams.ma Num/EqParams.mma +IntMap/Mapiter.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma IntMap/Mapaxioms.ma Lists/List.ma ZArith/ZArith.ma +Reals/PartSum.ma Reals/PartSum.mma +Num/Definitions.mma Coq.ma +Num/DiscrAxioms.mma Coq.ma Num/NSyntax.ma Num/Params.ma +ZArith/Zsqrt.mma Coq.ma ZArith/ZArith_base.ma +Reals/Rderiv.ma Reals/Rderiv.mma +Wellfounded/Union.ma Wellfounded/Union.mma +Arith/Gt.mma Arith/Le.ma Arith/Lt.ma Arith/Plus.ma Coq.ma +Arith/Even.ma Arith/Even.mma +Sets/Constructive_sets.mma Coq.ma Sets/Ensembles.ma +Reals/Rseries.ma Reals/Rseries.mma +Arith/Minus.ma Arith/Minus.mma +Lists/List.mma Arith/Le.ma Coq.ma +ZArith/ZArith_base.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Wf_Z.ma ZArith/ZArith_dec.ma ZArith/Zabs.ma ZArith/Zbool.ma ZArith/Zcompare.ma ZArith/Zeven.ma ZArith/Zhints.ma ZArith/Zmin.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma ZArith/auxiliary.ma +Num/Axioms.ma Num/Axioms.mma +Reals/SplitRmult.ma Reals/SplitRmult.mma +Reals/Rsqrt_def.ma Reals/Rsqrt_def.mma +Arith/Plus.mma Arith/Le.ma Arith/Lt.ma Coq.ma +IntMap/Map.ma IntMap/Map.mma +Init/Logic_Type.mma Coq.ma Init/Datatypes.ma Init/Logic.ma +Reals/Raxioms.mma Coq.ma Reals/Rdefinitions.ma ZArith/ZArith_base.ma +ZArith/BinInt.ma ZArith/BinInt.mma +Reals/Rtrigo.ma Reals/Rtrigo.mma +Reals/Ranalysis1.mma Coq.ma Reals/Rbase.ma Reals/Rderiv.ma Reals/Rfunctions.ma Reals/Rlimit.ma +Reals/Cos_plus.ma Reals/Cos_plus.mma +Bool/Bvector.ma Bool/Bvector.mma +Logic/Hurkens.mma Coq.ma +Num/OppAxioms.ma Num/OppAxioms.mma +Relations/Relations.mma Coq.ma Relations/Operators_Properties.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma +Reals/R_sqr.mma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma +Arith/Peano_dec.ma Arith/Peano_dec.mma +Reals/Rprod.ma Reals/Rprod.mma +Num/NeqDef.ma Num/NeqDef.mma +Arith/Bool_nat.mma Arith/Compare_dec.ma Arith/Peano_dec.ma Bool/Sumbool.ma Coq.ma +ZArith/ZArith_dec.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma +Arith/Euclid.mma Arith/Compare_dec.ma Arith/Mult.ma Arith/Wf_nat.ma Coq.ma +ZArith/Zbinary.ma ZArith/Zbinary.mma +Logic/Decidable.ma Logic/Decidable.mma +Logic/RelationalChoice.mma Coq.ma +Sets/Infinite_sets.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Finite_sets_facts.ma Sets/Image.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma +Init/Prelude.ma Init/Prelude.mma +Num/Nat/Axioms.mma Coq.ma Num/EqAxioms.ma Num/NSyntax.ma Num/Params.ma +Reals/Rsigma.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma +ZArith/Zbinary.mma Bool/Bvector.ma Coq.ma ZArith/ZArith.ma ZArith/Zpower.ma +Sets/Ensembles.mma Coq.ma +Reals/Binomial.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma +Logic/ClassicalChoice.mma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalDescription.ma Logic/RelationalChoice.ma +Reals/R_Ifp.ma Reals/R_Ifp.mma +Logic/ProofIrrelevance.ma Logic/ProofIrrelevance.mma +Reals/MVT.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtopology.ma +Reals/RiemannInt_SF.ma Reals/RiemannInt_SF.mma +Num/Axioms.mma Coq.ma Num/EqParams.ma Num/NSyntax.ma Num/Params.ma +ZArith/Zdiv.ma ZArith/Zdiv.mma +Num/GeAxioms.mma Coq.ma Num/Axioms.ma Num/LtProps.ma +Sets/Permut.ma Sets/Permut.mma +Num/DiscrAxioms.ma Num/DiscrAxioms.mma +Sets/Cpo.ma Sets/Cpo.mma +Reals/Rtrigo_calc.mma Coq.ma Reals/R_sqrt.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +Arith/Even.mma Coq.ma +Reals/Sqrt_reg.mma Coq.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma +ZArith/Zabs.ma ZArith/Zabs.mma +Sorting/Heap.ma Sorting/Heap.mma +Reals/Ranalysis3.mma Coq.ma Reals/Ranalysis1.ma Reals/Ranalysis2.ma Reals/Rbase.ma Reals/Rfunctions.ma +Num/Params.mma Coq.ma +Reals/RiemannInt.mma Arith/Max.ma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/RiemannInt_SF.ma Reals/SeqSeries.ma +Logic/Classical_Pred_Set.ma Logic/Classical_Pred_Set.mma +Logic/Classical_Type.ma Logic/Classical_Type.mma +Init/Prelude.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma Init/Peano.ma Init/Specif.ma Init/Wf.ma +Wellfounded/Lexicographic_Product.mma Coq.ma Logic/Eqdep.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma +Logic/Decidable.mma Coq.ma +Reals/Reals.mma Coq.ma Reals/Integration.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +Num/Leibniz/Params.ma Num/Leibniz/Params.mma +NArith/Pnat.mma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma +Arith/EqNat.mma Coq.ma +IntMap/Allmaps.ma IntMap/Allmaps.mma +ZArith/Zhints.ma ZArith/Zhints.mma +Sets/Constructive_sets.ma Sets/Constructive_sets.mma +ZArith/Zeven.mma Coq.ma ZArith/BinInt.ma +Num/GeAxioms.ma Num/GeAxioms.mma +Num/Params.ma Num/Params.mma +Reals/Rdefinitions.mma Coq.ma ZArith/ZArith_base.ma +Reals/Rsigma.ma Reals/Rsigma.mma +ZArith/Zbool.mma Bool/Sumbool.ma Coq.ma ZArith/BinInt.ma ZArith/ZArith_dec.ma ZArith/Zcompare.ma ZArith/Zeven.ma ZArith/Zorder.ma +Reals/RIneq.mma Coq.ma Reals/Raxioms.ma +Sets/Multiset.mma Arith/Plus.ma Coq.ma Sets/Permut.ma +Coq.ma preamble.ma +Relations/Relation_Operators.mma Coq.ma Lists/List.ma Relations/Relation_Definitions.ma +Num/LeAxioms.mma Coq.ma Num/Axioms.ma Num/LtProps.ma +Init/Wf.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma +Logic/Berardi.mma Coq.ma +Logic/JMeq.ma Logic/JMeq.mma +ZArith/Zmisc.mma Bool/Bool.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma +Arith/Minus.mma Arith/Le.ma Arith/Lt.ma Coq.ma +Arith/Le.ma Arith/Le.mma +Num/AddProps.ma Num/AddProps.mma +IntMap/Addec.ma IntMap/Addec.mma +Logic/ClassicalFacts.mma Coq.ma +Sets/Integers.ma Sets/Integers.mma +ZArith/Znat.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Peano_dec.ma Coq.ma Logic/Decidable.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zorder.ma +ZArith/ZArith.ma ZArith/ZArith.mma +Num/LeProps.ma Num/LeProps.mma +Num/Nat/NSyntax.mma Coq.ma +Reals/ArithProp.mma Arith/Div2.ma Arith/Even.ma Coq.ma Reals/Rbase.ma Reals/Rbasic_fun.ma +Logic/Berardi.ma Logic/Berardi.mma +Num/OppProps.mma Coq.ma +Relations/Rstar.mma Coq.ma +Reals/SplitRmult.mma Coq.ma Reals/Rbase.ma +IntMap/Mapsubset.ma IntMap/Mapsubset.mma +Arith/Div.mma Arith/Compare_dec.ma Arith/Le.ma Coq.ma +Bool/Zerob.ma Bool/Zerob.mma +Wellfounded/Well_Ordering.ma Wellfounded/Well_Ordering.mma +Reals/Rsqrt_def.mma Bool/Sumbool.ma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma +Reals/Ranalysis2.ma Reals/Ranalysis2.mma +Reals/R_sqrt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rsqrt_def.ma +Sorting/Permutation.ma Sorting/Permutation.mma +Reals/Rlimit.ma Reals/Rlimit.mma +IntMap/Mapsubset.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapiter.ma ZArith/ZArith.ma +Arith/Compare.mma Arith/Arith.ma Arith/Compare_dec.ma Arith/Min.ma Arith/Peano_dec.ma Arith/Wf_nat.ma Coq.ma +Sets/Finite_sets.ma Sets/Finite_sets.mma +Relations/Newman.ma Relations/Newman.mma +NArith/NArith.mma Coq.ma NArith/BinNat.ma NArith/BinPos.ma +Lists/List.ma Lists/List.mma +ZArith/ZArith_base.ma ZArith/ZArith_base.mma +Sets/Infinite_sets.ma Sets/Infinite_sets.mma +Reals/Alembert.ma Reals/Alembert.mma +Sets/Relations_1.mma Coq.ma +ZArith/ZArith_dec.ma ZArith/ZArith_dec.mma +Bool/Bool.mma Coq.ma +ZArith/Zcompare.mma Arith/Gt.ma Arith/Lt.ma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma +Reals/NewtonInt.ma Reals/NewtonInt.mma +Num/DiscrProps.mma Coq.ma Num/DiscrAxioms.ma Num/LtProps.ma +Sorting/Heap.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma Sorting/Sorting.ma +Reals/R_sqrt.ma Reals/R_sqrt.mma +Sets/Powerset_facts.ma Sets/Powerset_facts.mma +Reals/Rfunctions.ma Reals/Rfunctions.mma +Bool/IfProp.ma Bool/IfProp.mma +Relations/Operators_Properties.ma Relations/Operators_Properties.mma +Reals/NewtonInt.mma Coq.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +ZArith/Zcomplements.mma Arith/Wf_nat.ma Coq.ma Lists/List.ma ZArith/ZArith_base.ma +Bool/Zerob.mma Arith/Arith.ma Bool/Bool.ma Coq.ma +Sets/Relations_2.ma Sets/Relations_2.mma +Init/Specif.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma +ZArith/Zabs.mma Arith/Arith.ma Coq.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/ZArith_dec.ma ZArith/Zorder.ma +Logic/Eqdep.ma Logic/Eqdep.mma +Bool/BoolEq.ma Bool/BoolEq.mma +ZArith/Zlogarithm.ma ZArith/Zlogarithm.mma +NArith/BinNat.ma NArith/BinNat.mma +Reals/MVT.ma Reals/MVT.mma +Lists/MonoList.mma Arith/Le.ma Coq.ma +NArith/NArith.ma NArith/NArith.mma +Num/GeProps.ma Num/GeProps.mma +Arith/Between.ma Arith/Between.mma +Num/GeProps.mma Coq.ma +preamble.ma coq.ma +Reals/PSeries_reg.ma Reals/PSeries_reg.mma +Num/SubProps.ma Num/SubProps.mma +Num/Leibniz/NSyntax.ma Num/Leibniz/NSyntax.mma +NArith/BinPos.ma NArith/BinPos.mma +Reals/AltSeries.ma Reals/AltSeries.mma +Reals/SeqProp.mma Arith/Max.ma Coq.ma Logic/Classical.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma +Logic/ClassicalDescription.ma Logic/ClassicalDescription.mma +IntMap/Mapcanon.ma IntMap/Mapcanon.mma +Reals/Rgeom.mma Coq.ma Reals/R_sqrt.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +Wellfounded/Transitive_Closure.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma +Sets/Relations_3.mma Coq.ma Sets/Relations_1.ma Sets/Relations_2.ma +Reals/SeqSeries.mma Arith/Max.ma Coq.ma Reals/Alembert.ma Reals/AltSeries.ma Reals/Binomial.ma Reals/Cauchy_prod.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rcomplete.ma Reals/Rfunctions.ma Reals/Rprod.ma Reals/Rseries.ma Reals/Rsigma.ma Reals/SeqProp.ma +Arith/Lt.ma Arith/Lt.mma +Reals/RList.ma Reals/RList.mma +Arith/Between.mma Arith/Le.ma Arith/Lt.ma Coq.ma +Num/Definitions.ma Num/Definitions.mma +Arith/Plus.ma Arith/Plus.mma +Reals/R_sqr.ma Reals/R_sqr.mma +Init/Peano.mma Coq.ma Init/Datatypes.ma Init/Logic.ma Init/Notations.ma +Logic/Classical_Pred_Type.mma Coq.ma Logic/Classical_Prop.ma +Reals/Binomial.ma Reals/Binomial.mma +Arith/Min.mma Arith/Arith.ma Coq.ma +Relations/Relation_Operators.ma Relations/Relation_Operators.mma +Reals/RIneq.ma Reals/RIneq.mma +Lists/MonoList.ma Lists/MonoList.mma +Sets/Powerset.mma Coq.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma +Arith/Min.ma Arith/Min.mma +Reals/PSeries_reg.mma Arith/Even.ma Arith/Max.ma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/SeqSeries.ma +Reals/Rtrigo_def.ma Reals/Rtrigo_def.mma +IntMap/Adalloc.ma IntMap/Adalloc.mma +Wellfounded/Well_Ordering.mma Coq.ma Logic/Eqdep.ma +IntMap/Map.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma ZArith/ZArith.ma +Reals/SplitAbsolu.ma Reals/SplitAbsolu.mma +Arith/Compare_dec.ma Arith/Compare_dec.mma +Arith/Euclid.ma Arith/Euclid.mma +Arith/EqNat.ma Arith/EqNat.mma +Num/SubProps.mma Coq.ma +Lists/ListSet.mma Coq.ma Lists/List.ma +Sets/Finite_sets_facts.mma Arith/Gt.ma Arith/Lt.ma Coq.ma Logic/Classical_Type.ma Sets/Classical_sets.ma Sets/Constructive_sets.ma Sets/Finite_sets.ma Sets/Powerset.ma Sets/Powerset_Classical_facts.ma Sets/Powerset_facts.ma +IntMap/Mapfold.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma +ZArith/Zorder.mma Arith/Arith.ma Coq.ma Logic/Decidable.ma NArith/BinPos.ma ZArith/BinInt.ma ZArith/Zcompare.ma +Logic/Classical_Pred_Set.mma Coq.ma Logic/Classical_Prop.ma +Num/Leibniz/NSyntax.mma Coq.ma Num/Params.ma +Sets/Relations_2_facts.mma Coq.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma Sets/Relations_2.ma +Reals/Integration.mma Coq.ma Reals/NewtonInt.ma Reals/RiemannInt.ma Reals/RiemannInt_SF.ma +Sets/Partial_Order.mma Coq.ma Sets/Ensembles.ma Sets/Relations_1.ma +Reals/Rfunctions.mma Coq.ma Reals/ArithProp.ma Reals/R_Ifp.ma Reals/R_sqr.ma Reals/Rbase.ma Reals/Rbasic_fun.ma Reals/SplitAbsolu.ma Reals/SplitRmult.ma ZArith/Zpower.ma +IntMap/Mapcard.ma IntMap/Mapcard.mma +Arith/Arith.ma Arith/Arith.mma +Arith/Max.ma Arith/Max.mma +Reals/Exp_prop.mma Arith/Div2.ma Arith/Even.ma Arith/Max.ma Coq.ma Reals/PSeries_reg.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +Reals/Rbase.ma Reals/Rbase.mma +Bool/IfProp.mma Bool/Bool.ma Coq.ma +ZArith/BinInt.mma Arith/Mult.ma Arith/Plus.ma Coq.ma NArith/BinNat.ma NArith/BinPos.ma NArith/Pnat.ma +Num/Nat/Axioms.ma Num/Nat/Axioms.mma +Relations/Relations.ma Relations/Relations.mma +ZArith/Zeven.ma ZArith/Zeven.mma +ZArith/Zbool.ma ZArith/Zbool.mma +Init/Wf.ma Init/Wf.mma +Reals/R_Ifp.mma Coq.ma Reals/Rbase.ma +IntMap/Adalloc.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma ZArith/ZArith.ma +Sets/Powerset_facts.mma Coq.ma Sets/Constructive_sets.ma Sets/Cpo.ma Sets/Ensembles.ma Sets/Partial_Order.ma Sets/Powerset.ma Sets/Relations_1.ma Sets/Relations_1_facts.ma +Init/Datatypes.mma Coq.ma Init/Logic.ma Init/Notations.ma +Logic/Diaconescu.mma Bool/Bool.ma Coq.ma Logic/ChoiceFacts.ma Logic/ClassicalFacts.ma +IntMap/Mapaxioms.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Map.ma ZArith/ZArith.ma +Arith/Mult.mma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Plus.ma Coq.ma +Logic/Classical_Prop.mma Coq.ma Logic/ProofIrrelevance.ma +Num/Leibniz/EqAxioms.mma Coq.ma Num/NSyntax.ma +Num/Nat/NeqDef.ma Num/Nat/NeqDef.mma +Logic/ProofIrrelevance.mma Coq.ma Logic/Hurkens.ma +ZArith/auxiliary.ma ZArith/auxiliary.mma +Sets/Image.ma Sets/Image.mma +Num/NeqAxioms.ma Num/NeqAxioms.mma +Reals/Rtrigo_def.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_fun.ma Reals/SeqSeries.ma +Relations/Operators_Properties.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma +IntMap/Maplists.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Fset.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapc.ma IntMap/Mapcanon.ma IntMap/Mapcard.ma IntMap/Mapfold.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma +Num/OppProps.ma Num/OppProps.mma +Logic/ClassicalChoice.ma Logic/ClassicalChoice.mma +Reals/RiemannInt_SF.mma Coq.ma Logic/Classical_Prop.ma Reals/Ranalysis.ma Reals/Rbase.ma Reals/Rfunctions.ma +Num/LtProps.mma Coq.ma Num/AddProps.ma Num/Axioms.ma Num/NeqProps.ma +Reals/SeqProp.ma Reals/SeqProp.mma +Reals/SeqSeries.ma Reals/SeqSeries.mma +Bool/DecBool.mma Coq.ma +Init/Specif.ma Init/Specif.mma +Init/Logic.mma Coq.ma Init/Notations.ma +Logic/Classical_Prop.ma Logic/Classical_Prop.mma +Setoids/Setoid.ma Setoids/Setoid.mma +IntMap/Mapfold.ma IntMap/Mapfold.mma +Logic/Classical_Type.mma Coq.ma Logic/Classical_Pred_Type.ma Logic/Classical_Prop.ma +Setoids/Setoid.mma Coq.ma +Init/Logic.ma Init/Logic.mma +IntMap/Adist.ma IntMap/Adist.mma +ZArith/Wf_Z.ma ZArith/Wf_Z.mma +Sets/Uniset.ma Sets/Uniset.mma +Logic/Eqdep_dec.ma Logic/Eqdep_dec.mma +Sorting/Sorting.ma Sorting/Sorting.mma +Reals/Cauchy_prod.mma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma +ZArith/Zsqrt.ma ZArith/Zsqrt.mma +Reals/Ranalysis2.mma Coq.ma Reals/Ranalysis1.ma Reals/Rbase.ma Reals/Rfunctions.ma +IntMap/Mapiter.ma IntMap/Mapiter.mma +Logic/Hurkens.ma Logic/Hurkens.mma +Sets/Relations_3_facts.ma Sets/Relations_3_facts.mma +ZArith/Zwf.mma Arith/Wf_nat.ma Coq.ma ZArith/ZArith_base.ma +Reals/AltSeries.mma Arith/Max.ma Coq.ma Reals/PartSum.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma +Logic/RelationalChoice.ma Logic/RelationalChoice.mma +Reals/Ranalysis3.ma Reals/Ranalysis3.mma +IntMap/Fset.mma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Map.ma ZArith/ZArith.ma +IntMap/Adist.mma Arith/Arith.ma Arith/Min.ma Bool/Bool.ma Coq.ma IntMap/Addr.ma ZArith/ZArith.ma +Arith/Compare.ma Arith/Compare.mma +Reals/Rtrigo_alt.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma +ZArith/Wf_Z.mma Arith/Wf_nat.ma Coq.ma ZArith/BinInt.ma ZArith/Zcompare.ma ZArith/Zmisc.ma ZArith/Znat.ma ZArith/Zorder.ma +Wellfounded/Disjoint_Union.mma Coq.ma Relations/Relation_Operators.ma +Sets/Uniset.mma Bool/Bool.ma Coq.ma Sets/Permut.ma +Sets/Relations_2_facts.ma Sets/Relations_2_facts.mma +Num/NSyntax.mma Coq.ma Num/Params.ma +Arith/Wf_nat.ma Arith/Wf_nat.mma +Reals/Rcomplete.ma Reals/Rcomplete.mma +Reals/Rtrigo.mma Coq.ma Logic/Classical_Prop.ma Reals/Cos_plus.ma Reals/Cos_rel.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_alt.ma Reals/Rtrigo_def.ma Reals/Rtrigo_fun.ma Reals/SeqSeries.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma +Reals/Rpower.mma Coq.ma Reals/Exp_prop.ma Reals/MVT.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Ranalysis4.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rsqrt_def.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +ZArith/Znumtheory.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma ZArith/Zdiv.ma +Reals/Cos_plus.mma Arith/Max.ma Coq.ma Reals/Cos_rel.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma +Reals/Rtrigo_fun.ma Reals/Rtrigo_fun.mma +Wellfounded/Wellfounded.ma Wellfounded/Wellfounded.mma +Arith/Bool_nat.ma Arith/Bool_nat.mma +Sets/Relations_1_facts.ma Sets/Relations_1_facts.mma +Arith/Gt.ma Arith/Gt.mma +Reals/Rtrigo_calc.ma Reals/Rtrigo_calc.mma +Reals/Reals.ma Reals/Reals.mma +Num/Nat/NSyntax.ma Num/Nat/NSyntax.mma +Sets/Relations_3.ma Sets/Relations_3.mma +Reals/Exp_prop.ma Reals/Exp_prop.mma +Num/EqAxioms.mma Coq.ma Num/EqParams.ma Num/NSyntax.ma Num/Params.ma +Num/Leibniz/EqAxioms.ma Num/Leibniz/EqAxioms.mma +Num/NSyntax.ma Num/NSyntax.mma +Num/NeqProps.ma Num/NeqProps.mma +Arith/Le.mma Coq.ma +ZArith/Zpower.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zcomplements.ma +IntMap/Mapcard.mma Arith/Arith.ma Arith/Peano_dec.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma +Reals/Ranalysis.ma Reals/Ranalysis.mma +IntMap/Lsort.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Map.ma IntMap/Mapiter.ma Lists/List.ma ZArith/ZArith.ma +ZArith/Znumtheory.ma ZArith/Znumtheory.mma +Reals/Ranalysis4.mma Coq.ma Reals/Exp_prop.ma Reals/Ranalysis1.ma Reals/Ranalysis3.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo.ma Reals/SeqSeries.ma +Num/NeqParams.ma Num/NeqParams.mma +ZArith/Zmin.ma ZArith/Zmin.mma +Sets/Classical_sets.mma Coq.ma Logic/Classical_Type.ma Sets/Constructive_sets.ma Sets/Ensembles.ma +Arith/Wf_nat.mma Arith/Lt.ma Coq.ma +Lists/TheoryList.mma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Bool/DecBool.ma Coq.ma Lists/List.ma +Sets/Finite_sets.mma Coq.ma Sets/Constructive_sets.ma Sets/Ensembles.ma +Num/NeqProps.mma Coq.ma Num/EqAxioms.ma Num/EqParams.ma Num/NeqAxioms.ma Num/NeqParams.ma +Sets/Powerset_Classical_facts.ma Sets/Powerset_Classical_facts.mma +Reals/Rbasic_fun.mma Coq.ma Reals/R_Ifp.ma Reals/Rbase.ma +Init/Logic_Type.ma Init/Logic_Type.mma +Sets/Permut.mma Coq.ma +Num/EqParams.mma Coq.ma Num/Params.ma +Logic/ClassicalDescription.mma Coq.ma Logic/Classical.ma +Init/Notations.mma Coq.ma +NArith/BinPos.mma Coq.ma +Reals/PartSum.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rcomplete.ma Reals/Rfunctions.ma Reals/Rseries.ma +Logic/JMeq.mma Coq.ma Logic/Eqdep.ma +Wellfounded/Transitive_Closure.ma Wellfounded/Transitive_Closure.mma +ZArith/Zdiv.mma Coq.ma ZArith/ZArith_base.ma ZArith/Zbool.ma ZArith/Zcomplements.ma +ZArith/Zwf.ma ZArith/Zwf.mma +Num/LtProps.ma Num/LtProps.mma +Lists/TheoryList.ma Lists/TheoryList.mma +Sorting/Permutation.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma +Reals/Rpower.ma Reals/Rpower.mma +Wellfounded/Inverse_Image.ma Wellfounded/Inverse_Image.mma +Reals/Rbasic_fun.ma Reals/Rbasic_fun.mma +Arith/Div2.ma Arith/Div2.mma +Reals/Rlimit.mma Coq.ma Logic/Classical_Prop.ma Reals/Rbase.ma Reals/Rfunctions.ma +Wellfounded/Lexicographic_Product.ma Wellfounded/Lexicographic_Product.mma +Reals/Cos_rel.mma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rtrigo_def.ma Reals/SeqSeries.ma +Reals/Ranalysis.mma Coq.ma Reals/Exp_prop.ma Reals/MVT.ma Reals/PSeries_reg.ma Reals/RList.ma Reals/R_sqrt.ma Reals/Ranalysis1.ma Reals/Ranalysis2.ma Reals/Ranalysis3.ma Reals/Ranalysis4.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rgeom.ma Reals/Rpower.ma Reals/Rsqrt_def.ma Reals/Rtopology.ma Reals/Rtrigo.ma Reals/Rtrigo_calc.ma Reals/Rtrigo_reg.ma Reals/SeqSeries.ma Reals/Sqrt_reg.ma +Reals/SplitAbsolu.mma Coq.ma Reals/Rbasic_fun.ma +Num/LeAxioms.ma Num/LeAxioms.mma +ZArith/Znat.ma ZArith/Znat.mma +Relations/Rstar.ma Relations/Rstar.mma +Logic/ChoiceFacts.mma Coq.ma +Bool/Bool.ma Bool/Bool.mma +Wellfounded/Union.mma Coq.ma Relations/Relation_Definitions.ma Relations/Relation_Operators.ma Wellfounded/Transitive_Closure.ma +Bool/Bvector.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma +IntMap/Mapaxioms.ma IntMap/Mapaxioms.mma +IntMap/Maplists.ma IntMap/Maplists.mma +Wellfounded/Inclusion.mma Coq.ma Relations/Relation_Definitions.ma +Logic/Diaconescu.ma Logic/Diaconescu.mma +Reals/Cos_rel.ma Reals/Cos_rel.mma +Reals/Rcomplete.mma Arith/Max.ma Coq.ma Reals/Rbase.ma Reals/Rfunctions.ma Reals/Rseries.ma Reals/SeqProp.ma +Logic/Eqdep.mma Coq.ma +Relations/Relation_Definitions.ma Relations/Relation_Definitions.mma +IntMap/Mapcanon.mma Arith/Arith.ma Bool/Bool.ma Bool/Sumbool.ma Coq.ma IntMap/Addec.ma IntMap/Addr.ma IntMap/Adist.ma IntMap/Fset.ma IntMap/Lsort.ma IntMap/Map.ma IntMap/Mapaxioms.ma IntMap/Mapcard.ma IntMap/Mapiter.ma IntMap/Mapsubset.ma Lists/List.ma ZArith/ZArith.ma +Num/GtAxioms.ma Num/GtAxioms.mma +Arith/Factorial.ma Arith/Factorial.mma +Arith/Arith.mma Arith/Between.ma Arith/Compare_dec.ma Arith/Factorial.ma Arith/Gt.ma Arith/Le.ma Arith/Lt.ma Arith/Minus.ma Arith/Mult.ma Arith/Peano_dec.ma Arith/Plus.ma Coq.ma +Wellfounded/Inverse_Image.mma Coq.ma +IntMap/Mapc.ma IntMap/Mapc.mma +Bool/BoolEq.mma Bool/Bool.ma Coq.ma +Reals/Sqrt_reg.ma Reals/Sqrt_reg.mma +Sorting/Sorting.mma Coq.ma Lists/List.ma Relations/Relations.ma Sets/Multiset.ma Sorting/Permutation.ma +NArith/Pnat.ma NArith/Pnat.mma +Arith/Div.ma Arith/Div.mma +Sets/Multiset.ma Sets/Multiset.mma +Num/Leibniz/Params.mma Coq.ma +Reals/Rgeom.ma Reals/Rgeom.mma +ZArith/Zcomplements.ma ZArith/Zcomplements.mma +Logic/Classical_Pred_Type.ma Logic/Classical_Pred_Type.mma +Sets/Relations_2.mma Coq.ma Sets/Relations_1.ma +Reals/Cauchy_prod.ma Reals/Cauchy_prod.mma +Num/EqAxioms.ma Num/EqAxioms.mma +Bool/DecBool.ma Bool/DecBool.mma +Logic/Eqdep_dec.mma Coq.ma +coq.ma diff --git a/helm/software/matita/contribs/procedural/Makefile.common b/helm/software/matita/contribs/procedural/Makefile.common index ec1cb7d1a..5402df5db 100644 --- a/helm/software/matita/contribs/procedural/Makefile.common +++ b/helm/software/matita/contribs/procedural/Makefile.common @@ -1,10 +1,10 @@ BIN = ../../../ -DIR=$(shell basename $$PWD) +DIR = $(shell basename $$PWD) -H=@ +H = @ -MATITAOPTIONS= +MATITAOPTIONS = TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt @@ -26,7 +26,7 @@ clean.opt: $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(H)$(RM) $(MAS) depend: - $$(H)(BIN)matitadep $(MATITAOPTIONS) + $(H)(BIN)matitadep $(MATITAOPTIONS) depend.opt: $(H)$(BIN)matitadep.opt $(MATITAOPTIONS) -- 2.39.2