From 3fc67e00e7b0959d4e6b0321309fff8c589f0ed2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 17 Feb 2017 11:30:02 +0100
Subject: Compatiblity with Ltac as a plugin.

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 39fe3d6..5316a30 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -27,6 +27,7 @@ open Feedback
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
+open Ltac_plugin
 open Genarg
 open Stdarg
 open Tacarg
-- 
cgit v1.2.3