diff options
| author | Enrico Tassi | 2020-05-05 19:27:12 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-05-05 19:27:12 +0200 |
| commit | bc79d319d38f766a6b7bbeb1f1071b046642089b (patch) | |
| tree | 1f2f52d171b0694dfecf0f7003ae96630e5837ca /proofs/refiner.mli | |
| parent | f4532cf12ce96a6e60115641356582ff44ea525f (diff) | |
| parent | d87f8d10d089c3a33ddb36a71ab6fc082d0d1140 (diff) | |
Merge PR #12227: Spring cleaning of the tactic compatibility layer
Reviewed-by: gares
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 66eae1db81..3471f38e9e 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. } *) @@ -32,7 +32,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic (** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies |