X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=4df3a5bd4bb5d1384ec3dceb1489bcad2bccc4e6;hb=e01753bf730b3c4e50df0655f7940f8720b16524;hp=6a4b07aabfaf0daf9f6b7dedc8a4644a73fae22f;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 6a4b07aab..4df3a5bd4 100644
--- 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