aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/vernacextend.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/vernacextend.ml4')
-rw-r--r--grammar/vernacextend.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index ad8929657..433779302 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -113,7 +113,7 @@ let declare_command loc s c nt cl =
} >> ]
open Pcaml
-open PcamlSig
+open PcamlSig (* necessary for camlp4 *)
EXTEND
GLOBAL: str_item;