new cicEnvironment implementation

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 6a4b07aabfaf0daf9f6b7dedc8a4644a73fae22f..4df3a5bd4bb5d1384ec3dceb1489bcad2bccc4e6 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -58,7 +58,7 @@ let whd context =
        )
     | C.Var (uri,exp_named_subst) as t ->
        let o,_ = 
-         CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph 
+         CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
        in
        (match o with
            C.Constant _ -> raise ReferenceToConstant
@@ -84,7 +84,7 @@ let whd context =
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,exp_named_subst) as t ->
        let o,_ = 
-         CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph 
+         CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
        in
        (match o with
            C.Constant (_,Some body,_,_) ->
@@ -126,7 +126,7 @@ let whd context =
             C.MutConstruct (_,_,j,_) -> whdaux l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
               match o with
                  C.InductiveDefinition (tl,ingredients,r) ->
                    let (_,_,arity,_) = List.nth tl i in