5 files changed, 11 insertions, 15 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index d242264a91..51b99b9935 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -18,12 +18,12 @@ Module Type Int.
 
   Bind Scope Int_scope with t.
 
-  Parameter zero : t.
-  Parameter one : t.
-  Parameter plus : t -> t -> t.
-  Parameter opp : t -> t.
-  Parameter minus : t -> t -> t.
-  Parameter mult : t -> t -> t.
+  Parameter Inline zero : t.
+  Parameter Inline one : t.
+  Parameter Inline plus : t -> t -> t.
+  Parameter Inline opp : t -> t.
+  Parameter Inline minus : t -> t -> t.
+  Parameter Inline mult : t -> t -> t.
 
   Notation "0" := zero : Int_scope.
   Notation "1" := one : Int_scope.
@@ -39,10 +39,10 @@ Module Type Int.
 
   (** Int should also be ordered: *)
 
-  Parameter le : t -> t -> Prop.
-  Parameter lt : t -> t -> Prop.
-  Parameter ge : t -> t -> Prop.
-  Parameter gt : t -> t -> Prop.
+  Parameter Inline le : t -> t -> Prop.
+  Parameter Inline lt : t -> t -> Prop.
+  Parameter Inline ge : t -> t -> Prop.
+  Parameter Inline gt : t -> t -> Prop.
   Notation "x <= y" := (le x y): Int_scope.
   Notation "x < y" := (lt x y) : Int_scope.
   Notation "x >= y" := (ge x y) : Int_scope.
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 06c80a8256..4ffbd5aa8b 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 open Names
 
 let module_refl_name = "ReflOmegaCore"
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 6dc5d9f7e5..a452b1a917 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 
 (** Coq objects used in romega *)
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 53f6f42c8e..5fd9c94194 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 
 DECLARE PLUGIN "romega_plugin"
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 1a53862ec4..517df41d93 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 open Pp
 open Util
 open Const_omega
@@ -1016,7 +1015,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list =
 
   Tactics.generalize
     (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >>
-  Tactics.change_concl (EConstr.of_constr reified) >>
+  Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >>
   Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >>
   show_goal >>
   (if unsafe then