X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicSubstitution.ml;h=a7124d4a3186d6512014c0f37a6e695e884401c1;hb=a4f6e8b443d8a676bd2bfbf7f29369e070298aa0;hp=aff9437575beab1ea7e65aacacf4175dc42ddf84;hpb=21d58727027699d8617a7faab912843756b585ed;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index aff943757..a7124d4a3 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -205,7 +205,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
         with
          Not_found ->
           let params =
-           let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+           let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
            (match obj with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable (_,_,_,params) -> params
@@ -254,7 +254,7 @@ prerr_endline "---- END\n\n " ;
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst')  ->
        let params =
-        let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match obj with
             C.Constant (_,_,_,params) -> params
           | C.Variable _ -> raise ReferenceToVariable
@@ -268,7 +268,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 CicUniv.empty_ugraph in
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
@@ -282,7 +282,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 CicUniv.empty_ugraph in
+        let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable