X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2Fncic2astMatcher.ml;h=41d9aa08c7e08c0609d170e9e726c79b59045777;hb=57c7d6ef239b4c2b070721715887684adf41159c;hp=099e0b26a2c8f2d1ffd30415830448b33348a7b8;hpb=5149063488e3771fb55c198e0ecef5fb5aaaab67;p=helm.git diff --git a/helm/software/components/ng_cic_content/ncic2astMatcher.ml b/helm/software/components/ng_cic_content/ncic2astMatcher.ml index 099e0b26a..41d9aa08c 100644 --- a/helm/software/components/ng_cic_content/ncic2astMatcher.ml +++ b/helm/software/components/ng_cic_content/ncic2astMatcher.ml @@ -34,14 +34,14 @@ struct struct type cic_mask_t = Blob - | Uri of UriManager.uri + | NRef of NReference.reference | Appl of cic_mask_t list let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) let mask_of_cic = function | NCic.Appl tl -> Appl (List.map (fun _ -> Blob) tl), tl - | NCic.Const nref -> Uri (NCic2OCic.ouri_of_reference nref), [] + | NCic.Const nref -> NRef nref, [] | _ -> Blob, [] let tag_of_term t = @@ -49,7 +49,8 @@ struct Hashtbl.hash mask, tl let mask_of_appl_pattern = function - | Ast.UriPattern uri -> Uri uri, [] + | Ast.UriPattern uri -> NRef (OCic2NCic.reference_of_oxuri uri), [] + | Ast.NRefPattern nref -> NRef nref, [] | Ast.ImplicitPattern | Ast.VarPattern _ -> Blob, [] | Ast.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl @@ -70,6 +71,7 @@ struct | Ast.ImplicitPattern | Ast.VarPattern _ -> PatternMatcher.Variable | Ast.UriPattern _ + | Ast.NRefPattern _ | Ast.ApplPattern _ -> PatternMatcher.Constructor end