debian version 0.0.5-6

[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 4df3a5bd4bb5d1384ec3dceb1489bcad2bccc4e6..04067ccbfdfbb27663920b6ca3c2e46c9309f3b5 100644 (file)
--- 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