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) "")
in
(match o with
C.Constant _ -> raise ReferenceToConstant
- | C.Variable (_,_,_,params) -> params
+ | C.Variable (_,_,_,params,_) -> params
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
in
(match o with
- C.Constant (_,_,_,params) -> params
+ C.Constant (_,_,_,params,_) -> params
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,_,_,params) -> params
+ | C.CurrentProof (_,_,_,_,params,_) -> params
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_) -> params
+ | C.InductiveDefinition (_,params,_,_) -> params
)
in
let exp_named_subst' =
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_) -> params
+ | C.InductiveDefinition (_,params,_,_) -> params
)
in
let exp_named_subst' =
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- | C.Variable (_,None,_,_) ->
+ | C.Variable (_,None,_,_,_) ->
let t' = unwind k e ens t in
if s = [] then t' else
C.Appl (t'::(RS.from_stack_list ~unwind s))
- | C.Variable (_,Some body,_,_) ->
+ | C.Variable (_,Some body,_,_,_) ->
let ens' = push_exp_named_subst k e ens exp_named_subst in
reduce (0, [], ens', body, s)
)
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
in
match o with
- C.Constant (_,Some body,_,_) ->
+ C.Constant (_,Some body,_,_,_) ->
let ens' = push_exp_named_subst k e ens exp_named_subst in
(* constants are closed *)
reduce (0, [], ens', body, s)
- | C.Constant (_,None,_,_) ->
+ | C.Constant (_,None,_,_,_) ->
let t' = unwind k e ens t in
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,body,_,_) ->
+ | C.CurrentProof (_,_,body,_,_,_) ->
let ens' = push_exp_named_subst k e ens exp_named_subst in
(* constants are closed *)
reduce (0, [], ens', body, s)
CicEnvironment.get_cooked_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