From 320363315e350bf427054d837a02b4d97f015199 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 22 Dec 2018 01:45:30 +0100
Subject: Fix #9272: `Unset Nested Proofs Allowed` does not capture nested
 `Instance` proofs.

We forbid commands that may open proofs inside proofs.
---
 stm/stm.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 32c6c7d959..27feac9adb 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2993,7 +2993,14 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       (* Unknown: we execute it, check for open goals and propagate sideeff *)
       | VtUnknown, VtNow ->
           let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
-          let id = VCS.new_node ~id:newtip () in
+          if not (get_allow_nested_proofs ()) && in_proof then
+            "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on."
+            |> Pp.str
+            |> (fun s -> (UserError (None, s), Exninfo.null))
+            |> State.exn_on ~valid:Stateid.dummy Stateid.dummy
+            |> Exninfo.iraise
+          else
+            let id = VCS.new_node ~id:newtip () in
           let head_id = VCS.get_branch_pos head in
           let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
           let step () =
-- 
cgit v1.2.3