From 13dd3f8ebaf90f30afbcb48034e5bdd90c825765 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 20:33:32 +0100
Subject: Fixing compilation with old versions of CAMLP5.

---
 parsing/g_ltac.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 79392195fb..d1992c57bb 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -310,10 +310,11 @@ open Stdarg
 open Constrarg
 open Vernacexpr
 open Vernac_classifier
+open Goptions
 
 let print_info_trace = ref None
 
-let _ = let open Goptions in declare_int_option {
+let _ = declare_int_option {
   optsync = true;
   optdepr = false;
   optname = "print info trace";
-- 
cgit v1.2.3