- let terms, terms' =
- List.split (List.map (fun (context, t) -> t, reduction context t) terms)
- in
- let where' =
- ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
- ~where:where
- in
- CicMetaSubst.apply_subst subst where' in
+ let pairs, metasenv, ugraph =
+ List.fold_left
+ (fun (pairs, metasenv, ugraph) (context, t) ->
+ let reduction, metasenv, ugraph = reduction context metasenv ugraph in
+ ((t, reduction context t) :: pairs), metasenv, ugraph)
+ ([], metasenv, ugraph)
+ terms
+ in
+ let terms, terms' = List.split pairs in
+ let where' =
+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+ ~where:where
+ in
+ CicMetaSubst.apply_subst subst where', metasenv, ugraph
+ in