From 9e26743cf40cdfd85317d2826ee05373d8670082 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 27 Jun 2018 21:34:39 +0200
Subject: Split the Ssrmatching module between code and grammar rules.

Fixes #7857.
---
 plugins/ssr/ssrparser.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 347a1e4e2..6b183dab1 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -962,6 +962,7 @@ END
 (* the default simpl and unfold tactics would erase blindly.               *)
 
 open Ssrmatching_plugin.Ssrmatching
+open Ssrmatching_plugin.G_ssrmatching
 
 let pr_wgen = function 
   | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id
-- 
cgit v1.2.3