3 files changed, 5 insertions, 5 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index fbed1df17..d97dea039 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -226,7 +226,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> Term.constr
   val parse_term : Term.constr -> parse_term
-  val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+  val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val get_scalar : Term.constr -> Bigint.bigint option
 end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index ca23ed6c4..a452b1a91 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -113,7 +113,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : Term.constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
+    val parse_rel : [ `NF ] Proofview.Goal.t -> Term.constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val get_scalar : Term.constr -> Bigint.bigint option
   end
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index fdcd62299..575634174 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Util
-open Proofview.Notations
 open Const_omega
 module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -1029,7 +1028,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
   Tactics.apply (EConstr.of_constr (Lazy.force coq_I))
 
 let total_reflexive_omega_tactic unsafe =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
@@ -1043,4 +1042,5 @@ let total_reflexive_omega_tactic unsafe =
   if !debug then display_systems systems_list;
   resolution unsafe env reified_goal systems_list
   with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
-  end }
+  end
+