X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Fncic2astMatcher.ml;h=f6617451ddecc98a3b751fa95997255a9b906344;hb=09c63c35520ceea6f0caaa0be856a3eaff46bb88;hp=2245e34295791f082d1e4a451b4c811aba52ba4d;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_cic_content/ncic2astMatcher.ml b/matita/components/ng_cic_content/ncic2astMatcher.ml
index 2245e3429..f6617451d 100644
--- a/matita/components/ng_cic_content/ncic2astMatcher.ml
+++ b/matita/components/ng_cic_content/ncic2astMatcher.ml
@@ -25,11 +25,8 @@
 
 (* $Id: acic2astMatcher.ml 9271 2008-11-28 18:28:58Z fguidi $ *)
 
-module Ast = CicNotationPt
-module Util = CicNotationUtil
-
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
+module Ast = NotationPt
+module Util = NotationUtil
 
 module Matcher32 =
 struct
@@ -40,8 +37,6 @@ struct
     | NRef of NReference.reference
     | Appl of cic_mask_t list
 
-    let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
-
     let mask_of_cic = function
       | NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl
       | NCic.Const nref -> NRef nref, []
@@ -52,7 +47,6 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Ast.UriPattern uri -> NRef (!reference_of_oxuri uri), []
       | Ast.NRefPattern nref -> NRef nref, []
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> Blob, []
@@ -65,7 +59,7 @@ struct
     type pattern_t = Ast.cic_appl_pattern
     type term_t = NCic.term
 
-    let string_of_pattern = CicNotationPp.pp_cic_appl_pattern
+    let string_of_pattern = NotationPp.pp_cic_appl_pattern
     let string_of_term t =
      (*CSC: ??? *)
      NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
@@ -73,7 +67,6 @@ struct
     let classify = function
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> PatternMatcher.Variable
-      | Ast.UriPattern _
       | Ast.NRefPattern _
       | Ast.ApplPattern _ -> PatternMatcher.Constructor
   end