diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 2 |
3 files changed, 4 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 197d69a481..695e103082 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -77,7 +77,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) - (Proofview.V82.tactic (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))) + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) end let clenv_pose_dependent_evars ?(with_evars=false) clenv = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 75c3436cf4..6a0ba30bbf 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -37,6 +37,8 @@ let refiner ~check = CProfile.profile2 refiner_key (refiner ~check) else refiner ~check +let refiner ~check c = Proofview.V82.tactic (refiner ~check c) + (*********************) (* Tacticals *) (*********************) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 66eae1db81..d4f2239a59 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -22,7 +22,7 @@ val project : 'a sigma -> evar_map val pf_env : Goal.goal sigma -> Environ.env val pf_hyps : Goal.goal sigma -> named_context -val refiner : check:bool -> Constr.t -> tactic +val refiner : check:bool -> Constr.t -> unit Proofview.tactic (** {6 Tacticals. } *) |