From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/romega/refl_omega.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins/romega/refl_omega.ml') diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index d1824978..e6034806 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,6 +8,7 @@ open Pp open Util +open Constr open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -1036,13 +1037,13 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = let decompose_tactic = decompose_tree env context solution_tree in Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check reified Term.DEFAULTcast >> + Tactics.convert_concl_no_check reified DEFAULTcast >> Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> show_goal >> (if unsafe then (* Trust the produced term. Faster, but might fail later at Qed. Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast + Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast else Tactics.normalise_vm_in_concl) >> Tactics.apply (Lazy.force coq_I) -- cgit v1.2.3