new cicEnvironment implementation

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e0fd252a6b6b8a254c25b60bd9a82f76eed7fd8a..e456a1731b226d3e66cd4718a12aeb19dab0f165 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -354,7 +354,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
          else
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
@@ -386,7 +386,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.Const (uri,exp_named_subst) ->
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph 
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant (_,_,_,params) -> params
@@ -402,7 +402,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.MutInd (uri,i,exp_named_subst) ->
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph 
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
@@ -418,7 +418,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.MutConstruct (uri,i,j,exp_named_subst) ->
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
@@ -543,7 +543,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
          else
           ( let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
             match o with
               C.Constant _ -> raise ReferenceToConstant
@@ -601,7 +601,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
   *)
      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
         (let o,_ = 
-          CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph 
+          CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
         in
          match o with
             C.Constant (_,Some body,_,_) ->
@@ -659,7 +659,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
               let (arity, r) =
                let o,_ = 
-                 CicEnvironment.get_cooked_obj mutind CicUniv.empty_ugraph
+                 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                in
                  match o with
                       C.InductiveDefinition (tl,ingredients,r) ->