diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 20 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 2 |
2 files changed, 11 insertions, 11 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index d242264a9..51b99b993 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/refl_omega.ml b/plugins/romega/refl_omega.ml index 1a53862ec..60e6e7de7 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1016,7 +1016,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 |