X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=04067ccbfdfbb27663920b6ca3c2e46c9309f3b5;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=4df3a5bd4bb5d1384ec3dceb1489bcad2bccc4e6;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 4df3a5bd4..04067ccbf 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -31,7 +31,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
@@ -64,8 +64,8 @@ let whd context =
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_,_) ->
+         | C.Variable (_,None,_,_,_) -> if l = [] then t else C.Appl (t::l)
+         | C.Variable (_,Some body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
@@ -87,11 +87,11 @@ let whd context =
 	  CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
 	in
        (match o with
-           C.Constant (_,Some body,_,_) ->
+           C.Constant (_,Some body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.Constant _ -> if l = [] then t else C.Appl (t::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_,_) ->
+         | C.CurrentProof (_,_,body,_,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
@@ -128,7 +128,7 @@ let whd context =
              let (arity, r) =
 	       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
               match o with
-                 C.InductiveDefinition (tl,ingredients,r) ->
+                 C.InductiveDefinition (tl,ingredients,r,_) ->
                    let (_,_,arity,_) = List.nth tl i in
                     (arity,r)
                | _ -> raise WrongUriToInductiveDefinition