diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 4 |
2 files changed, 2 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 8cb0a8b463..6497b6ff98 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -896,7 +896,7 @@ let interp_rpattern s = function let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t -type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option +type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 let loc_of_cpattern = loc_ofCG let cpattern_of_term (c, t) ist = c, t, Some ist diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 93a8c48435..8672c55767 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -5,9 +5,7 @@ open Goal open Environ open Evd open Constr - -open Ltac_plugin -open Tacexpr +open Genintern (** ******** Small Scale Reflection pattern matching facilities ************* *) |