diff options
| author | Pierre-Marie Pédrot | 2018-11-21 13:03:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-21 13:03:27 +0100 |
| commit | 4d0fea2ededb11d79f4f1abcc1595f9cec20d6dd (patch) | |
| tree | bbd47886f4649999ecad9f21ffb6ff55869f0132 /plugins/ssrmatching | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
| parent | 417641e48129c9ba8656c622c9b64cd32641e7de (diff) | |
Merge PR #8998: [legacy proof engine] Remove some cruft.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 63b7e1783e..93a8c48435 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -230,7 +230,7 @@ sig val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern - val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern + val interp_rpattern : Geninterp.interp_sign -> Goal.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern val pr_rpattern : rpattern -> Pp.t val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern @@ -238,7 +238,7 @@ sig val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern - val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern + val interp_ssrterm : Geninterp.interp_sign -> Goal.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern val pr_ssrterm : cpattern -> Pp.t end |