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) "")
)
| 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)
| 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
)
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