X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=b9809335cf491d493c683dd81f69fe842398ac42;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=2ae4fd00e1664976c1fa7fa0e954cc624a79b330;hpb=34113d572c334c351ba66f4b05db503eed4d48f2;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 2ae4fd00e..b9809335c 100644
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -195,7 +195,8 @@ struct
   struct
     type pattern_t = Pt.term
     type term_t = Pt.term
-    let classify = function
+    let rec classify = function
+      | Pt.AttributedTerm (_, t) -> classify t
       | Pt.Variable _ -> Variable
       | Pt.Magic _
       | Pt.Layout _
@@ -373,20 +374,23 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | GrafiteAst.UriPattern uri -> Uri uri, []
-      | GrafiteAst.VarPattern _ -> Blob, []
-      | GrafiteAst.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
+      | Pt.UriPattern uri -> Uri uri, []
+      | Pt.ImplicitPattern
+      | Pt.VarPattern _ -> Blob, []
+      | Pt.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 = GrafiteAst.cic_appl_pattern
+    type pattern_t = Pt.cic_appl_pattern
     type term_t = Cic.annterm
 
     let classify = function
-      | GrafiteAst.VarPattern _ -> Variable
-      | _ -> Constructor
+      | Pt.ImplicitPattern
+      | Pt.VarPattern _ -> Variable
+      | Pt.UriPattern _
+      | Pt.ApplPattern _ -> Constructor
   end
 
   module M = Matcher (Pattern32)
@@ -399,7 +403,8 @@ struct
           List.map2
             (fun p t ->
               match p with
-              | GrafiteAst.VarPattern name -> name, t
+              | Pt.ImplicitPattern -> Util.fresh_name (), t
+              | Pt.VarPattern name -> name, t
               | _ -> assert false)
             pl matched_terms
         in