function
[],[] -> raise Not_found
| what::tl1,with_what::tl2 ->
- if equality t what then with_what else find_image_aux (tl1,tl2)
+ if equality what t then with_what else find_image_aux (tl1,tl2)
| _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
in
find_image_aux (what,with_what)
function
[],[] -> raise Not_found
| what::tl1,with_what::tl2 ->
- if equality t what then with_what else find_image_aux (tl1,tl2)
+ if equality what t then with_what else find_image_aux (tl1,tl2)
| _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
in
find_image_aux (what,with_what)
function
[],[] -> raise Not_found
| what::tl1,with_what::tl2 ->
- if equality t what then with_what else find_image_aux (tl1,tl2)
+ if equality what t then with_what else find_image_aux (tl1,tl2)
| _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
in
find_image_aux (what,with_what)
| Cic.Appl (he::tl) -> hd_delta_beta context tl he
| t -> cannot_delta_expand t
in
- let context, where =
+ let context, where' =
match what with
None -> context, where
| Some what ->
(ProofEngineTypes.Fail
("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))
in
- hd_delta_beta context [] where
+ 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
;;