transcript: improved debuugging facilities

orocedural/Coq: we escaped the non-ASCII7 characters

diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 5e737a14aa313f7922740fe01b6c4c838993e1c5..793da99404c568c5b6cf48e57ffe2effb938ed67 100644 (file)
--- 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 61ce486f942424361aa3e3f912184f93bb07bead..01bfffa3025d00f013bdf7c3a826fd12bb651cbe 100644 (file)
--- 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 b9bfc6109e2ba69afa2472938ed4b31accf8ce36..4bcb2d53f22f4a2a4bc036c0f0c6e30061ce5ed1 100644 (file)
--- 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 1f9b36866a50cbdca3246631ee4eed9a2afa1109..f5c4a49f8ccabe1f2f95f89554904a2c9f2440be 100644 (file)
--- 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 (file)
index 0000000..e259494
--- /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 5ef75dab70f4be01abf2d47740260e830ef2c448..5b3b234730fff1c8d61a06764aa22125ed10ffbb 100644 (file)
--- 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 <dir> ] [ <package> | <conf_file> ]*" in
    let help_C = " set working directory to <dir>" 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 57f7d16ae1bff92121e55c2b05bbefc357a99600..0ef38a919b55604548d120eaf607004d2d961e52 100644 (file)
--- 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 52456c5594d761957d7d3576683952dd975b3ddb..4627cf9a277cb7e33e4d35e01422776f8e863206 100644 (file)
--- 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 0894e8eea9392d7e5806a4fdfcc7ff00d2a2bfe7..c50415feca2653e25dc697251418bda17eb4e0fb 100644 (file)
--- 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 7ab50d0141c6eea18a84f33f92d9f1ea9f8f3999..82db6eb1f8a962abdbb51a479922297412eabb74 100644 (file)
--- 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 4efee3045d893dd5134145fac4cad55fa3cbe70a..283a2fd5bf3d5005e7c552f5a2afe6bc89d92fff 100644 (file)
--- 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 18782ade80cdd61d0b0cf691e6f320e0fbf21a5b..ac333d7c3deb6bed82f733659caab85254b05d57 100644 (file)
--- 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 da44e41880cd7d938ba287f6521ed080d4314060..2d835257e9d657e5b493082edd989df34d415dde 100644 (file)
--- 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 d4704676bde70ba800325017e5f86039e8683525..b032806c85f7050d199d4f077d695d2966d09056 100644 (file)
--- 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 b85e455907148ed1daa2083fff6048f79e4380f0..db3a0a34ea9395d19d24d4a8bc4d7bda8e819827 100644 (file)
--- 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 34bd26086460da79afd165d7f89e4f54dd686d94..b773d21631edf8a0a31043a83e28daa8911e3b4f 100644 (file)
--- 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 32f52201e09e38c4f875ca36d1c13fb3bd35bb06..c1a764ae9b6fe22bc5c7893808040412e10b85b1 100644 (file)
--- 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 a1c27a484a80a791c293f73a0a1dabf37f2d8526..87df305f6bbae4efa094f7e4c1edcc6d72abd329 100644 (file)
--- 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 539d29adf93fd72ee85774e0dca6f10340e84d66..484ab7dd4ac9deed53b699782639fa488bc2058b 100644 (file)
--- 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 570b0350d6aca986770e4160e9bb3d0f0cd94485..37d8af215c10c8395a4832cadafd750b6c6f3edf 100644 (file)
--- 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 ab193ad2e595aca47269be87dfb5b0aa08611964..97df3d2633d7308f27836467317facaecb353632 100644 (file)
--- 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 92a6310b87d944080dd244b8a9697a6c5861d5e3..2dca10d37b367adf865fc79272ea7fd063ae2340 100644 (file)
--- 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 1d274647a6117412fb524a9b0aa08dc97ffe5310..cef5a51acc9b73f0af4028f4ec384bcff2d8a670 100644 (file)
--- 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 0eeec13113ad612a7d8c7c748db0fb9e5d1472e9..5f6e88a08a78efa8be31bc69d2866e45342b4d16 100644 (file)
--- 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 (file)
index 0000000..14c7744
--- /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 ec1cb7d1a65928df541e566025fa344ac244b755..5402df5dbb599998e1ed2d90f44f7dbc5767d190 100644 (file)
--- 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)