- let replace context where=
-(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
-(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
-(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
- try
- let terms' = List.map (reduction context) terms in
- ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
- ~where:where
- with
- _ -> where
+ let replace lift context where=
+ (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
+ (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
+ (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei*)
+ try
+ let terms = List.fold_left
+ (fun acc t ->
+ try
+ (CicSubstitution.delift lift t) :: acc
+ with Failure _ -> acc
+ ) [] terms
+ in
+ let terms' = List.map (reduction context) terms in
+ ProofEngineReduction.replace
+ ~equality:(=) ~what:terms ~with_what:terms' ~where:where
+ with
+ _ -> where