From cf35c36c341d7f1f615b3e11e6aab64a7fa6a5bf Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 19 Apr 2011 17:11:35 +0000
Subject: Declarative mode: fix escape and return.

The declarative mode should now work almost like in v8.3

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14029 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/g_decl_mode.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/decl_mode/g_decl_mode.ml4')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a133089f8f..aa187cc749 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -74,12 +74,12 @@ let vernac_decl_proof () =
     end
 
 (* spiwack: some bureaucracy is not performed here *)
-let vernac_return () = 
+let vernac_return () =
   Decl_proof_instr.return_from_tactic_mode () ;
   Proof_global.set_proof_mode "Declarative" ;
   Vernacentries.print_subgoals ()
 
-let vernac_proof_instr instr = 
+let vernac_proof_instr instr =
   Decl_proof_instr.proof_instr instr;
   Vernacentries.print_subgoals ()
 
-- 
cgit v1.2.3