aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect')
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml41
1 files changed, 1 insertions, 0 deletions
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