aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-22 11:40:57 +0100
committerPierre-Marie Pédrot2018-11-23 13:59:15 +0100
commitbb4daa4af0515f3041203c5bcc0a1d8cd1123e5a (patch)
treeaa36956741fcc87ab5a69b086a983d005a0d1c9f /plugins/ssrmatching
parent6817d0da46adc07ad01b167d5362153d60e2f853 (diff)
Only use Coq API in coqpp.
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 3f0794fdd4..0dd17dfc15 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -11,7 +11,6 @@
{
open Ltac_plugin
-open Pcoq
open Pcoq.Constr
open Ssrmatching
open Ssrmatching.Internal