diff options
| author | Pierre-Marie Pédrot | 2020-05-12 12:13:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 12:18:19 +0200 |
| commit | 65551cdf811a1bf428fcdc7e3e5c51df0fffcb78 (patch) | |
| tree | 995028e052cf0e8b37214d18462dc1ce4c5e8067 /proofs/logic.mli | |
| parent | d31cb4d3e55da99d42abdc1f4129ddc03e1631c6 (diff) | |
Wrap the legacy refiner type into the Logic API.
Diffstat (limited to 'proofs/logic.mli')
| -rw-r--r-- | proofs/logic.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli index 5d21474394..e4fed22860 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -26,7 +26,7 @@ open Evd (** The primitive refiner. *) -val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map +val refiner : check:bool -> constr -> unit Proofview.tactic (** {6 Refiner errors. } *) |