From 3e8db9f159e534dd194817550f8b5664febc4477 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 12 Sep 2013 13:44:27 +0000
Subject: Unknown commands starting a proof were not setting the proof mode.

Fixes Orsay/Containers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16771 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 1bade01bbc..67e855327b 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1182,7 +1182,8 @@ let process_transaction verbosely (loc, expr) =
             then begin
               let bname = VCS.mk_branch_name x in
               VCS.commit id (Fork (x,bname,[]));
-              VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1))
+              VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
+              Proof_global.activate_proof_mode "Classic";
             end else begin
               VCS.commit id (Cmd (x,[]));
               VCS.propagate_sideff (Some x);
-- 
cgit v1.2.3