Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index b9a5b72f478dfbad467211e3935163647711c540..49d004ee0201d765c6a9445c172d38f24294091b 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -109,7 +109,7 @@ let rec pp t l =
        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
-         match CicEnvironment.get_obj uri with
+         match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
             C.InductiveDefinition (dl,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
               name ^ pp_exp_named_subst exp_named_subst l
@@ -119,7 +119,7 @@ let rec pp t l =
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
-         match CicEnvironment.get_obj uri with
+         match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
             C.InductiveDefinition (dl,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               let (id,_) = get_nth cons n2 in
@@ -132,7 +132,7 @@ let rec pp t l =
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
        let connames =
-        (match CicEnvironment.get_obj uri with
+        (match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
             C.InductiveDefinition (dl,_,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map (fun (id,_) -> id) cons