- 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
+ 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