C.Rel n as t ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
+ | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)
| C.Var (uri,exp_named_subst) ->
C.Rel n as t ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
- | Some (_,C.Def bo) ->
+ | Some (_,C.Def (bo,_)) ->
try_delta_expansion l t (S.lift n bo)
| None -> raise RelToHiddenHypothesis
)