Most warnings turned into errors and avoided

[helm.git] / matita / components / content_pres / content2presMatcher.ml

diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml
index 23f62092496d16eb7b47dd086d0ba0b017671616..f6319c73581cd7a2f9ea0aef618b48c022336386 100644 (file)
--- a/matita/components/content_pres/content2presMatcher.ml
+++ b/matita/components/content_pres/content2presMatcher.ml
@@ -25,12 +25,9 @@
 
 (* $Id$ *)
 
-open Printf
-
-module Ast = CicNotationPt
-module Env = CicNotationEnv
-module Pp = CicNotationPp
-module Util = CicNotationUtil
+module Ast = NotationPt
+module Env = NotationEnv
+module Util = NotationUtil
 
 let get_tag term0 =
   let subterms = ref [] in
@@ -39,7 +36,7 @@ let get_tag term0 =
     Ast.Implicit `JustOne
   in
   let rec aux t = 
-    CicNotationUtil.visit_ast 
+    NotationUtil.visit_ast 
       ~map_xref_option:(fun _ -> None)
       ~map_case_indty:(fun _ -> None)
       ~map_case_outtype:(fun _ _ -> None)
@@ -67,8 +64,11 @@ struct
       | _ -> PatternMatcher.Constructor
     let tag_of_pattern = get_tag
     let tag_of_term t = get_tag t
-    let string_of_term = CicNotationPp.pp_term
-    let string_of_pattern = CicNotationPp.pp_term
+
+    (* Debugging only *)
+    (*CSC: new NCicPp.status is the best I can do now *)
+    let string_of_term = NotationPp.pp_term (new NCicPp.status)
+    let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
   end
 
   module M = PatternMatcher.Matcher (Pattern21)
@@ -81,7 +81,7 @@ struct
       Ast.Variable (Ast.TermVar (name,Ast.Level 0))
     in
     let rec aux = function
-      | Ast.AttributedTerm (_, t) -> assert false
+      | Ast.AttributedTerm (_, _t) -> assert false
       | Ast.Literal _
       | Ast.Layout _ -> assert false
       | Ast.Variable v -> Ast.Variable v
@@ -101,8 +101,8 @@ struct
           | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
               name, (Env.NumType, Env.NumValue s)
           | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
-              name, (Env.StringType, Env.StringValue s)
-          | _ -> assert false)
+              name, (Env.StringType, Env.StringValue (Env.Ident s))
+          | _ -> assert false (* activate the DEBUGGING CODE below *))
         pl tl
     with Invalid_argument _ -> assert false
 
@@ -154,10 +154,19 @@ struct
       in
       magichooser candidates
     in
+(* DEBUGGING CODE 
+fun input ->
+let (fst,_)::_ = rows in
+prerr_endline ("RIGA: " ^ NotationPp.pp_term (new NCicPp.status) fst);
+prerr_endline ("CONTRO: " ^ NotationPp.pp_term (new NCicPp.status) input);
+*)
     M.compiler rows' match_cb (fun _ -> None)
+(* DEBUGGING CODE 
+input
+*)
 
   and compile_magic = function
-    | Ast.Fold (kind, p_base, names, p_rec) ->
+    | Ast.Fold (_kind, p_base, names, p_rec) ->
         let p_rec_decls = Env.declarations_of_term p_rec in
          (* LUCA: p_rec_decls should not contain "names" *)
         let acc_name = try List.hd names with Failure _ -> assert false in
@@ -172,7 +181,7 @@ struct
             let rec aux term =
               match compiled_rec term with
                 | None -> aux_base term
-                | Some (env', ctors', _) ->
+                | Some (env', _ctors', _) ->
                     begin
                        let acc = Env.lookup_term env' acc_name in
                        let env'' = Env.remove_name env' acc_name in
@@ -208,7 +217,7 @@ struct
           | Some (env', ctors', 0) ->
               let env' =
                 List.map
-                  (fun (name, (ty, v)) as binding ->
+                  (fun (name, (_ty, _v)) as binding ->
                     if List.exists (fun (name', _) -> name = name') p_opt_decls
                     then Env.opt_binding_some binding
                     else binding)