diff options
| author | Maxime Dénès | 2018-03-10 12:40:04 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 12:40:04 +0100 |
| commit | 33c5d8d00cb017c61141ee0d6b7cb8f672a3e691 (patch) | |
| tree | c7185ce535ef7c5438e79f1c4b81464c8367d6c9 /plugins/ssrmatching | |
| parent | 4d5c7243b4aea5b28358757e2d86c11334da6699 (diff) | |
| parent | 99129d2518bd9fe92051aa89138cbb57c839a270 (diff) | |
Merge PR #6869: [ssreflect] Fix module scoping problems due to packing and mli files.
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 07d0f97575..c55081e0f7 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 *) |