pattern matching over Ast.Case simplified:

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

diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml
index 3c6a61a6fb169958176aef607d6a359ffd879753..0e85618896833b254b52e12970ff81f6a3f96b72 100644 (file)
--- a/helm/software/components/content_pres/content2presMatcher.ml
+++ b/helm/software/components/content_pres/content2presMatcher.ml
@@ -38,7 +38,12 @@ let get_tag term0 =
     subterms := t :: !subterms ; 
     Ast.Implicit
   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