changed default parameter values...

[helm.git] / helm / ocaml / cic_notation / cicNotationMatcher.ml

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 9d879db5ea1c3ef6943b2ae2e36c04ec007ca95c..b9809335cf491d493c683dd81f69fe842398ac42 100644 (file)
--- 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 _
@@ -374,6 +375,7 @@ struct
 
     let mask_of_appl_pattern = function
       | Pt.UriPattern uri -> Uri uri, []
+      | Pt.ImplicitPattern
       | Pt.VarPattern _ -> Blob, []
       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 
@@ -385,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)
@@ -399,6 +403,7 @@ struct
           List.map2
             (fun p t ->
               match p with
+              | Pt.ImplicitPattern -> Util.fresh_name (), t
               | Pt.VarPattern name -> name, t
               | _ -> assert false)
             pl matched_terms