- (* we need this cause an equation E like
- F ?x => F ?y
- can add a meta for y in a goal without instantiating it
- P (F true) ----> P (F ?y)
- and this may cause duplicated in metasenvs
- demodulating again with E
- *)
- let bag, new_goals =
- List.fold_right
- (fun g (bag,acc) ->
- let bag, g = Equality.fix_metas_goal bag g in
- bag, g::acc)
- new_goals (bag,[])
- in