X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2Fcontent2presMatcher.ml;h=5eeed2667689d7e830bff041654d1bf1bee331ad;hb=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;hp=8b613a524775a32bab105d8c59bc126e1d5c676a;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/content_pres/content2presMatcher.ml b/matitaB/components/content_pres/content2presMatcher.ml
index 8b613a524..5eeed2667 100644
--- a/matitaB/components/content_pres/content2presMatcher.ml
+++ b/matitaB/components/content_pres/content2presMatcher.ml
@@ -40,6 +40,7 @@ let get_tag term0 =
   in
   let rec aux t = 
     NotationUtil.visit_ast 
+      ~clear_interpretation:true
       ~map_xref_option:(fun _ -> None)
       ~map_case_indty:(fun _ -> None)
       ~map_case_outtype:(fun _ _ -> None)
@@ -70,8 +71,9 @@ struct
 
     (* 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)
+    (*WR: can't guess a user id so I must use None *)
+    let string_of_term = NotationPp.pp_term (new NCicPp.status None)
+    let string_of_pattern = NotationPp.pp_term (new NCicPp.status None)
   end
 
   module M = PatternMatcher.Matcher (Pattern21)
@@ -103,7 +105,7 @@ struct
               name, (Env.TermType l, Env.TermValue t)
           | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
               name, (Env.NumType, Env.NumValue s)
-          | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
+          | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, `Ambiguous)) ->
               name, (Env.StringType, Env.StringValue (Env.Ident s))
           | _ -> assert false)
         pl tl