From dc4200a1c0e37a600537fd1809377a3137ce0cc3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 4 Nov 2016 19:34:40 +0100
Subject: Quick fix of tactic parsing while Load-ing in coqide.

Note that this is still broken when loading files containing C-zar scripts.
---
 toplevel/vernacentries.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c03f183ff5..ef530d590f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1906,6 +1906,10 @@ let vernac_check_guard () =
 exception End_of_input
 
 let vernac_load interp fname =
+  let interp x =
+    let proof_mode = Proof_global.get_default_proof_mode_name () in
+    Proof_global.activate_proof_mode proof_mode;
+    interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
     match Pcoq.Gram.entry_parse Pcoq.main_entry po with
-- 
cgit v1.2.3