X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcomponents%2Fcontent_pres%2Fcontent2presMatcher.ml;h=2a432d33255eb35d94e7f59a91361ac2cda62c11;hb=8161bcb58808e60658072bc3da83b62d1df2a223;hp=23f62092496d16eb7b47dd086d0ba0b017671616;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml
index 23f620924..2a432d332 100644
--- a/matita/components/content_pres/content2presMatcher.ml
+++ b/matita/components/content_pres/content2presMatcher.ml
@@ -27,10 +27,10 @@
 
 open Printf
 
-module Ast = CicNotationPt
-module Env = CicNotationEnv
-module Pp = CicNotationPp
-module Util = CicNotationUtil
+module Ast = NotationPt
+module Env = NotationEnv
+module Pp = NotationPp
+module Util = NotationUtil
 
 let get_tag term0 =
   let subterms = ref [] in
@@ -39,7 +39,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 +67,8 @@ 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
+    let string_of_term = NotationPp.pp_term
+    let string_of_pattern = NotationPp.pp_term
   end
 
   module M = PatternMatcher.Matcher (Pattern21)