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

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 91937ed34..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 _
@@ -386,8 +387,10 @@ struct
     type term_t = Cic.annterm
 
     let classify = function
+      | Pt.ImplicitPattern
       | Pt.VarPattern _ -> Variable
-      | _ -> Constructor
+      | Pt.UriPattern _
+      | Pt.ApplPattern _ -> Constructor
   end
 
   module M = Matcher (Pattern32)