X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Fncic2astMatcher.ml;h=4f65e9c03abb070f9ec9a01da572f17f26c23789;hb=dd627e471392375ca7b6dad78a931a8682e06dbe;hp=5acb8eb1349b5287361389dd49a03884b32a7a0b;hpb=c3b7b4c8697a146a3d734b5333d655a25a642cb9;p=helm.git

diff --git a/matita/components/ng_cic_content/ncic2astMatcher.ml b/matita/components/ng_cic_content/ncic2astMatcher.ml
index 5acb8eb13..4f65e9c03 100644
--- a/matita/components/ng_cic_content/ncic2astMatcher.ml
+++ b/matita/components/ng_cic_content/ncic2astMatcher.ml
@@ -28,9 +28,6 @@
 module Ast = NotationPt
 module Util = NotationUtil
 
-let reference_of_oxuri = ref (fun _ -> assert false);;
-let set_reference_of_oxuri f = reference_of_oxuri := f;;
-
 module Matcher32 =
 struct
   module Pattern32 =
@@ -50,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, []
@@ -63,22 +59,21 @@ struct
     type pattern_t = Ast.cic_appl_pattern
     type term_t = NCic.term
 
+    (* Debugging functions only *)
     let string_of_pattern = NotationPp.pp_cic_appl_pattern
     let string_of_term t =
-     (*CSC: ??? *)
-     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
+     (new NCicPp.status)#ppterm ~metasenv:[] ~subst:[] ~context:[] t
 
     let classify = function
       | Ast.ImplicitPattern
       | Ast.VarPattern _ -> PatternMatcher.Variable
-      | Ast.UriPattern _
       | Ast.NRefPattern _
       | Ast.ApplPattern _ -> PatternMatcher.Constructor
   end
 
   module M = PatternMatcher.Matcher (Pattern32)
 
-  let compiler rows =
+  let compiler status rows =
     let match_cb rows matched_terms constructors =
      HExtlib.list_findopt
       (fun (pl,pid) _ ->
@@ -98,7 +93,7 @@ struct
           | (name,t)::tl ->
              List.for_all
               (fun (name',t') ->
-                name <> name' || NCicReduction.alpha_eq [] [] [] t t'
+                name <> name' || NCicReduction.alpha_eq status [] [] [] t t'
               ) tl && check_non_linear_patterns tl
         in
          if check_non_linear_patterns env then