Added universes handling. The PRE_UNIVERSES tag may help ;)

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

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index c718524fc3b6d3e099a1eb64f45f7d6838fa51db..38f2e7a6d484c617b8e838d523a3372843e599c6 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -202,7 +202,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
         with
          Not_found ->
           let params =
-           let obj = CicEnvironment.get_obj uri in
+           let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
            (match obj with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable (_,_,_,params) -> params
@@ -251,7 +251,7 @@ prerr_endline "---- END\n\n " ;
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst')  ->
        let params =
-        let obj = CicEnvironment.get_obj uri in
+        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
         (match obj with
             C.Constant (_,_,_,params) -> params
           | C.Variable _ -> raise ReferenceToVariable
@@ -265,7 +265,7 @@ prerr_endline "---- END\n\n " ;
          C.Const (uri,exp_named_subst'')
     | C.MutInd (uri,typeno,exp_named_subst') ->
        let params =
-        let obj = CicEnvironment.get_obj uri in
+        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
         (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
@@ -279,7 +279,7 @@ prerr_endline "---- END\n\n " ;
          C.MutInd (uri,typeno,exp_named_subst'')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
        let params =
-        let obj = CicEnvironment.get_obj uri in
+        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
         (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable