From caa1e9278136bbf2c9353eeb415d331eee99c172 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 12 Mar 2015 17:29:51 +0100
Subject: Declarative mode: remove a superfluous [set_proof_mode].

It was probably creating bugs when trying to use [escape].
---
 plugins/decl_mode/decl_proof_instr.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 83dd10742d..ab5282e791 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1472,8 +1472,7 @@ let do_instr raw_instr pts =
     else pts
   in
   Proof_global.simple_with_current_proof (fun _ _ -> pts);
-  postprocess pts raw_instr.instr;
-  Proof_global.set_proof_mode "Declarative"
+  postprocess pts raw_instr.instr
 
 let proof_instr raw_instr =
   let p = Proof_global.give_me_the_proof () in
-- 
cgit v1.2.3