diff options
Diffstat (limited to 'tactics/rewrite.ml4')
| -rw-r--r-- | tactics/rewrite.ml4 | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 7260f1fd7e..32155f0543 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -742,16 +742,10 @@ let apply_strategy (s : strategy) env sigma concl cstr evars = evars := res.rew_evars; Some (Some (res.rew_prf, (res.rew_car, res.rew_rel, res.rew_from, res.rew_to))) -let evars_of_evi evi = - Intset.union (Evarutil.evars_of_term evi.evar_concl) - (match evi.evar_body with - | Evar_defined b -> Evarutil.evars_of_term b - | Evar_empty -> Intset.empty) - let split_evars_once sigma evd = Evd.fold (fun ev evi deps -> if Intset.mem ev deps then - Intset.union (evars_of_evi evi) deps + Intset.union (Class_tactics.evars_of_evi evi) deps else deps) evd sigma let existentials_of_evd evd = |