X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;fp=helm%2Focaml%2Fcic_notation%2FcicNotationMatcher.ml;h=2ae4fd00e1664976c1fa7fa0e954cc624a79b330;hb=34113d572c334c351ba66f4b05db503eed4d48f2;hp=9d879db5ea1c3ef6943b2ae2e36c04ec007ca95c;hpb=7df7f06d2bc2a3fe1fe95aab957cef480d27eb86;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 9d879db5e..2ae4fd00e 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -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