]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationMatcher.ml
snapshot, notably:
[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.ml
index 9d879db5ea1c3ef6943b2ae2e36c04ec007ca95c..2ae4fd00e1664976c1fa7fa0e954cc624a79b330 100644 (file)
@@ -373,19 +373,19 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Pt.UriPattern uri -> Uri uri, []
-      | Pt.VarPattern _ -> Blob, []
-      | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
+      | GrafiteAst.UriPattern uri -> Uri uri, []
+      | GrafiteAst.VarPattern _ -> Blob, []
+      | GrafiteAst.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 
     let tag_of_pattern p =
       let mask, pl = mask_of_appl_pattern p in
       Hashtbl.hash mask, pl
 
-    type pattern_t = Pt.cic_appl_pattern
+    type pattern_t = GrafiteAst.cic_appl_pattern
     type term_t = Cic.annterm
 
     let classify = function
-      | Pt.VarPattern _ -> Variable
+      | GrafiteAst.VarPattern _ -> Variable
       | _ -> Constructor
   end
 
@@ -399,7 +399,7 @@ struct
           List.map2
             (fun p t ->
               match p with
-              | Pt.VarPattern name -> name, t
+              | GrafiteAst.VarPattern name -> name, t
               | _ -> assert false)
             pl matched_terms
         in