- let rec substaux k what =
- let module C = Cic in
- let module S = CicSubstitution in
- function
- t when (equality t what) -> S.lift (k-1) with_what
- | C.Rel n as t -> t
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let find_image what t =
+ let rec find_image_aux =
+ function
+ [],[] -> raise Not_found
+ | what::tl1,with_what::tl2 ->
+ if equality t what then with_what else find_image_aux (tl1,tl2)
+ | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
+ in
+ find_image_aux (what,with_what)
+ in
+ let rec substaux k what t =
+ try
+ S.lift (k-1) (find_image what t)
+ with Not_found ->
+ match t with
+ C.Rel n as t -> t