- head_beta_reduce ~delta he'''
- | Cic.Cast (te,_) -> head_beta_reduce ~delta te
- | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
- let bo =
- match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
- Cic.Constant (_,bo,_,_,_) -> bo
- | Cic.Variable _ -> raise ReferenceToVariable
- | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
- | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- in
- (match bo with
- None -> t
- | Some bo ->
- head_beta_reduce
- ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
- | Cic.Const (uri,ens) as t when delta=true ->
- let bo =
- match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
- Cic.Constant (_,bo,_,_,_) -> bo
- | Cic.Variable _ -> raise ReferenceToVariable
- | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
- | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
- in
- (match bo with
- None -> t
- | Some bo ->
- head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo))
- | t -> t
+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce ~upto
+ ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
+ | Cic.Const (uri,ens) as t when delta=true ->
+ let bo =
+ match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+ Cic.Constant (_,bo,_,_,_) -> bo
+ | Cic.Variable _ -> raise ReferenceToVariable
+ | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+ | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ in
+ (match bo with
+ None -> t
+ | Some bo ->
+ head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
+ | t -> t