diff options
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 |