diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-12 13:44:27 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-12 13:44:27 +0000 |
| commit | 3e8db9f159e534dd194817550f8b5664febc4477 (patch) | |
| tree | 4beb62fb16285c036275c254160aeee0de58aca7 | |
| parent | 2de1c607e1e30a2d0057760fa4357e6adbe58c89 (diff) | |
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
| -rw-r--r-- | toplevel/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 1bade01bb..67e855327 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); |