X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2presMatcher.ml;h=23f62092496d16eb7b47dd086d0ba0b017671616;hb=09cfd99de377d72d7af96ad9815342a1b7b467a9;hp=3c6a61a6fb169958176aef607d6a359ffd879753;hpb=68f3812e06c04ddd664e86dbfd3a1c32f96a22d1;p=helm.git

diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml
index 3c6a61a6f..23f620924 100644
--- a/helm/software/components/content_pres/content2presMatcher.ml
+++ b/helm/software/components/content_pres/content2presMatcher.ml
@@ -36,9 +36,14 @@ let get_tag term0 =
   let subterms = ref [] in
   let map_term t =
     subterms := t :: !subterms ; 
-    Ast.Implicit
+    Ast.Implicit `JustOne
   in
-  let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
+  let rec aux t = 
+    CicNotationUtil.visit_ast 
+      ~map_xref_option:(fun _ -> None)
+      ~map_case_indty:(fun _ -> None)
+      ~map_case_outtype:(fun _ _ -> None)
+      ~special_k map_term t
   and special_k = function
     | Ast.AttributedTerm (_, t) -> aux t
     | _ -> assert false