aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/g_eqdecide.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/g_eqdecide.ml4')
-rw-r--r--plugins/ltac/g_eqdecide.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index b3bcc9984..2251a6620 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
(************************************************************************)
open Eqdecide
+open Stdarg
DECLARE PLUGIN "ltac_plugin"