diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e603480656..930048400a 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1049,7 +1049,7 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic unsafe = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Coqlib.check_required_library ["Coq";"romega";"ROmega"]; rst_omega_eq (); rst_omega_var (); |