diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 07d0f9757..c55081e0f 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -3,11 +3,13 @@ open Goal open Genarg -open Tacexpr open Environ open Evd open Constr +open Ltac_plugin +open Tacexpr + (** ******** Small Scale Reflection pattern matching facilities ************* *) (** Pattern parsing *) |