diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-15 16:41:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-06-16 10:27:47 +0200 |
| commit | 0437339ccac602d692b5b8c071b77ac756805520 (patch) | |
| tree | 755ba115f30cd91d067250468e5946dd1a0f4dc4 /plugins/ssr/ssrtacticals.mli | |
| parent | 4f6fd16c06b9e11bc2619a34c1629bd71aba76de (diff) | |
Removing Proof_type from the API.
Unluckily, this forces replacing a lot of code in plugins, because the API
defined the type of goals and tactics in Proof_type, and by the no-alias rule,
this was the only one. But Proof_type was already implicitly deprecated, so
that the API should have relied on Tacmach instead.
Diffstat (limited to 'plugins/ssr/ssrtacticals.mli')
| -rw-r--r-- | plugins/ssr/ssrtacticals.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 1d1887138..297cfdfdc 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -17,7 +17,7 @@ val tclSEQAT : int Misctypes.or_var * (('a * Ltac_plugin.Tacinterp.Value.t option list) * Ltac_plugin.Tacinterp.Value.t option) -> - Proof_type.tactic + Tacmach.tactic val tclCLAUSES : Ltac_plugin.Tacinterp.interp_sign -> @@ -27,7 +27,7 @@ val tclCLAUSES : Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val hinttac : Tacinterp.interp_sign -> @@ -42,5 +42,5 @@ val ssrdotac : Ssrmatching_plugin.Ssrmatching.cpattern option) option) list * Ssrast.ssrclseq) -> - Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma |