From e52303164660041690f6e05a110ff633007a1dd5 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 19 Mar 2015 11:33:10 +0100
Subject: Declarative mode: fix proof modes.

`end proof` changes the proof mode to `"Classic"`.
---
 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 ab5282e791..9d0b7f3466 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1446,6 +1446,7 @@ let rec postprocess pts instr =
 		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
     | Pend (B_elim ET_Case_analysis) -> goto_current_focus ()
+    | Pend B_proof -> Proof_global.set_proof_mode "Classic"
     | Pend _ -> ()
 
 let do_instr raw_instr pts =
-- 
cgit v1.2.3