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 6a4b07aabfaf0daf9f6b7dedc8a4644a73fae22f..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) "")
@@ -58,14 +58,14 @@ 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
          | 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)
@@ -84,14 +84,14 @@ 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,_,_) ->
+           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
        )
@@ -126,9 +126,9 @@ 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) ->
+                 C.InductiveDefinition (tl,ingredients,r,_) ->
                    let (_,_,arity,_) = List.nth tl i in
                     (arity,r)
                | _ -> raise WrongUriToInductiveDefinition