aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/g_class.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/g_class.ml4')
-rw-r--r--tactics/g_class.ml45
1 files changed, 5 insertions, 0 deletions
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 766593543..9ef154541 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -10,6 +10,11 @@
open Misctypes
open Class_tactics
+open Pcoq.Prim
+open Pcoq.Constr
+open Pcoq.Tactic
+open Stdarg
+open Constrarg
DECLARE PLUGIN "g_class"