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.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 
 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.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 
 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
 
 
 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
 
 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 T = Types

+module O = Options

 
 module UM = UriManager
 module NP = CicNotationPp
 
 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
    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.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, _, _) ->
       | 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))
 (* 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 
       | 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 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 [
    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
    ] 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
    
    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    = '"'
 }
 
 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 "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      }
    | 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
 
 %{
    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
 
 
    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.
 
 (*  
 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".
 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.
 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
 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
 *)
 
 (* 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 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 
 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).
 *)
 
 (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.
 
     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.
 *)
     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,
   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
   [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 *)
 
 
 (*#* 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".
 
 
 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 *)
 
 (*#* 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".
 
 
 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.
 
 
 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.
 
 
 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*)
 
 
 (*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".
 
 
 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".
 
 (*
 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.
 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
        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.
 *)
 
 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.
 
 (*
 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.
 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.
 *)
 
 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.
 *)
 
 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*)
 
 
 (*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*)
 
 
 (*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".
 
 
 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*)
 
 
 (*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".
 
 
 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*)
 
 
 (*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".
 
 
 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*)
 
 
 (*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".
 
 
 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 = ../../../
 
 BIN = ../../../
 

-DIR=$(shell basename $$PWD)
+DIR = $(shell basename $$PWD)

 
 

-H=@
+H = @

 
 

-MATITAOPTIONS=
+MATITAOPTIONS =

 
 TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt
 
 
 TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt
 


@@ -26,7 +26,7 @@ clean.opt:
        $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS)
        $(H)$(RM) $(MAS)
 depend:
        $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS)
        $(H)$(RM) $(MAS)
 depend:

-       $$(H)(BIN)matitadep $(MATITAOPTIONS)
+       $(H)(BIN)matitadep $(MATITAOPTIONS)

 depend.opt:
        $(H)$(BIN)matitadep.opt $(MATITAOPTIONS)
 
 depend.opt:
        $(H)$(BIN)matitadep.opt $(MATITAOPTIONS)