diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 13 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 41 | ||||
| -rw-r--r-- | tactics/tactics.mli | 6 |
4 files changed, 33 insertions, 29 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index bcf5e2947..b9c52144e 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1172,11 +1172,12 @@ let exact poly (c,clenv) = else let ctx = Evd.evar_universe_context clenv.evd in ctx, c - in - fun gl -> - tclTHEN (Refiner.tclEVARS (Evd.merge_universe_context (project gl) ctx)) - (exact_check c') gl - + in + Proofview.Goal.raw_enter begin fun gl -> + let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in + Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) (exact_check c') + end + (* Util *) let expand_constructor_hints env sigma lems = @@ -1465,7 +1466,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) match t with | Res_pf (c,cl) -> Proofview.V82.tactic (unify_resolve_gen poly flags (c,cl)) | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") - | Give_exact (c, cl) -> Proofview.V82.tactic (exact poly (c, cl)) + | Give_exact (c, cl) -> exact poly (c, cl) | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN (Proofview.V82.tactic (unify_resolve_gen poly flags (c,cl))) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 4674bd030..bb7d2f0d2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -35,7 +35,7 @@ let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_tr let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl - else exact_check c gl + else Proofview.V82.of_tactic (exact_check c) gl let assumption id = e_give_exact (mkVar id) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ba389faa9..23c37fb65 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -129,18 +129,18 @@ let convert_concl = Tacmach.convert_concl let convert_hyp = Tacmach.convert_hyp let thin_body = Tacmach.thin_body -let convert_gen pb x y gl = - try tclEVARS (pf_apply Evd.conversion gl pb x y) gl - with Reduction.NotConvertible -> - tclFAIL_lazy 0 (lazy (str"Not convertible")) - (* Adding more information in this message, even under the lazy, can result in huge *) - (* blowups, time and spacewise... (see autos used in DoubleCyclic.) 2.3s against 15s. *) - (* ++ Printer.pr_constr_env env x ++ *) - (* str" and " ++ Printer.pr_constr_env env y)) *) - gl - -let convert = convert_gen Reduction.CONV -let convert_leq = convert_gen Reduction.CUMUL +let convert_gen pb x y = + Proofview.Goal.raw_enter begin fun gl -> + try + let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in + Proofview.V82.tclEVARS sigma + with (* Reduction.NotConvertible *) _ -> + (** FIXME: Sometimes an anomaly is raised from conversion *) + Tacticals.New.tclFAIL 0 (str "Not convertible") +end + +let convert x y = convert_gen Reduction.CONV x y +let convert_leq x y = convert_gen Reduction.CUMUL x y let error_clear_dependency env id = function | Evarutil.OccurHypInSimpleClause None -> @@ -1194,16 +1194,19 @@ let cut_and_apply c = (* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) -let exact_check c gl = - let concl = (pf_concl gl) in - let ct = pf_type_of gl c in - try tclTHEN (convert_leq ct concl) (refine_no_check c) gl - with _ -> error "Not an exact proof." (*FIXME error handling here not the best *) - -let exact_no_check = refine_no_check let new_exact_no_check c = Proofview.Refine.refine (fun h -> (h, c)) +let exact_check c = + Proofview.Goal.raw_enter begin fun gl -> + (** We do not need to normalize the goal because we just check convertibility *) + let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let ct = Tacmach.New.pf_type_of gl c in + Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) + end + +let exact_no_check = refine_no_check + let vm_cast_no_check c gl = let concl = pf_concl gl in refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c1911819b..6574d88c5 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -45,8 +45,8 @@ val fix : Id.t option -> int -> tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic val cofix : Id.t option -> tactic -val convert : constr -> constr -> tactic -val convert_leq : constr -> constr -> tactic +val convert : constr -> constr -> unit Proofview.tactic +val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 Introduction tactics. } *) @@ -110,7 +110,7 @@ val intros_pattern_bound : val assumption : unit Proofview.tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic -val exact_check : constr -> tactic +val exact_check : constr -> unit Proofview.tactic val exact_proof : Constrexpr.constr_expr -> tactic (** {6 Reduction tactics. } *) |