| Cic.Appl (he::tl) -> hd_delta_beta context tl he
| t -> cannot_delta_expand t
in
- let context, where' =
+ let context_and_matched_term_list =
match what with
- None -> context, where
+ None -> [context, where]
| Some what ->
- try
+ let res =
ProofEngineHelpers.locate_in_term
~equality:first_is_the_expandable_head_of_second
what ~where context
- with
- ProofEngineHelpers.TermNotFound ->
+ in
+ if res = [] then
raise
(ProofEngineTypes.Fail
("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
+ else
+ res
in
- let reduced_term = hd_delta_beta context [] where' in
- match what with
- None -> reduced_term
- | Some what ->
- replace ~equality:first_is_the_expandable_head_of_second
- ~what:[what] ~with_what:[reduced_term] ~where
+ let reduced_terms =
+ List.map
+ (function (context,where) -> hd_delta_beta context [] where)
+ context_and_matched_term_list in
+ let whats = List.map snd context_and_matched_term_list in
+ replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
;;