From 6adbf7d9678257aa42ef0d3b30db2e484cd148ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 6 Oct 2014 08:46:53 +0200
Subject: decl_mode: stay in declarative mode

This solution is a bit dumb, but I guess does what one expects.
Each decl mode proof commands stays in proof mode.
---
 plugins/decl_mode/decl_proof_instr.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 41d93fc4fb..a21447fbb2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1463,6 +1463,7 @@ let do_instr raw_instr pts =
   postprocess pts raw_instr.instr;
   (* spiwack: this should restore a compatible semantics with
      v8.3 where we never stayed focused on 0 goal. *)
+  Proof_global.set_proof_mode "Declarative" ;
   Decl_mode.maximal_unfocus ()
 
 let proof_instr raw_instr =
-- 
cgit v1.2.3