X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=1c1532548589c22faee9f03d5a83d0c161cce4ee;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=08a4617f7c97cb672017e5215c9f9f4e2db78100;hpb=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 08a4617f7..1c1532548 100644
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -117,14 +117,12 @@ struct
 
   let variable_closure k =
     (fun matched_terms terms ->
-      prerr_endline "variable_closure";
       match terms with
       | hd :: tl -> k (hd :: matched_terms) tl
       | _ -> assert false)
 
   let constructor_closure ks k =
     (fun matched_terms terms ->
-      prerr_endline "constructor_closure";
       match terms with
       | t :: tl ->
           (try
@@ -187,9 +185,7 @@ struct
       | Pt.Variable _ -> Variable
       | Pt.Magic _
       | Pt.Layout _
-      | Pt.Literal _ as t ->
-          prerr_endline (CicNotationPp.pp_term t);
-          assert false
+      | Pt.Literal _ as t -> assert false
       | _ -> Constructor
     let tag_of_pattern = CicNotationTag.get_tag
     let tag_of_term = CicNotationTag.get_tag
@@ -260,7 +256,6 @@ struct
         candidates
     in
     let match_cb rows =
-      prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
       let candidates =
         List.map
           (fun (pl, pid) ->
@@ -317,7 +312,7 @@ struct
   struct
     type cic_mask_t =
       Blob
-    | Uri of string
+    | Uri of UriManager.uri
     | Appl of cic_mask_t list
 
     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
@@ -335,7 +330,7 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Pt.UriPattern s -> Uri s, []
+      | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), []
       | Pt.VarPattern _ -> Blob, []
       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 
@@ -355,7 +350,6 @@ struct
 
   let compiler rows =
     let match_cb rows =
-      prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows));
       let pl, pid = try List.hd rows with Not_found -> assert false in
       (fun matched_terms ->
         let env =