X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=e456a1731b226d3e66cd4718a12aeb19dab0f165;hb=a4f6e8b443d8a676bd2bfbf7f29369e070298aa0;hp=e0fd252a6b6b8a254c25b60bd9a82f76eed7fd8a;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e0fd252a6..e456a1731 100644
--- 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) ->