diff options
| -rw-r--r-- | tactics/tactics.ml | 15 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
3 files changed, 13 insertions, 8 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b266438f94..a47ee96a0a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1806,9 +1806,16 @@ let native_cast_no_check c gl = Tacmach.refine_no_check (Term.mkCast(c,Term.NATIVEcast,concl)) gl -let exact_proof c gl = - let c,ctx = Constrintern.interp_casted_constr (Tacmach.pf_env gl) (Tacmach.project gl) c (Tacmach.pf_concl gl) - in tclTHEN (tclEVARUNIVCONTEXT ctx) (Tacmach.refine_no_check c) gl +let exact_proof c = + let open Tacmach.New in + Proofview.Goal.nf_enter { enter = begin fun gl -> + Refine.refine { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in + let sigma = Evd.merge_universe_context sigma ctx in + Sigma.Unsafe.of_pair (c, sigma) + end } + end } let assumption = let open Context.Named.Declaration in @@ -4802,7 +4809,7 @@ end module New = struct open Proofview.Notations - let exact_proof c = Proofview.V82.tactic (exact_proof c) + let exact_proof c = exact_proof c open Genredexpr open Locus diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 87400bfdff..f6c001941c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -118,7 +118,7 @@ val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic val native_cast_no_check : constr -> tactic val exact_check : constr -> unit Proofview.tactic -val exact_proof : Constrexpr.constr_expr -> tactic +val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic (** {6 Reduction tactics. } *) @@ -436,6 +436,4 @@ module New : sig val reduce_after_refine : unit Proofview.tactic (** The reducing tactic called after {!refine}. *) - open Proofview - val exact_proof : Constrexpr.constr_expr -> unit tactic end diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0e5cef828b..23755dac1d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -504,7 +504,7 @@ let vernac_end_proof ?proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - let status = by (Tactics.New.exact_proof c) in + let status = by (Tactics.exact_proof c) in save_proof (Vernacexpr.(Proved(Opaque None,None))); if not status then Pp.feedback Feedback.AddedAxiom |