X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Facic2Ast.ml;h=d8ded0356fe7de783dfd34942ce4096c2b4e4eb4;hb=3bec70852905f57198cd5b659dc72d430c1c5d2c;hp=567b7f7bb6b38746d1f220251e0362d6d97691e4;hpb=dd8726f655e4fdad063baf456fcfc95f82e079cc;p=helm.git diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml index 567b7f7bb..d8ded0356 100644 --- a/helm/ocaml/cic_transformations/acic2Ast.ml +++ b/helm/ocaml/cic_transformations/acic2Ast.ml @@ -37,11 +37,12 @@ let sort_of_string = function | _ -> assert false let get_types uri = - match CicEnvironment.get_obj uri with - | Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l + let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with + | Cic.Constant _ -> assert false + | Cic.Variable _ -> assert false + | Cic.CurrentProof _ -> assert false + | Cic.InductiveDefinition (l,_,_) -> l let name_of_inductive_type uri i = let types = get_types uri in