From 49d73185be33ce521f4664e61d47b2db5d59d608 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 10 May 2018 10:16:14 +0200 Subject: Introduce an option to allow nested lemma, and turn it off by default. --- stm/stm.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 9ea6a305e..90360dce9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2771,6 +2771,14 @@ let process_back_meta_command ~newtip ~head oid aast w = VCS.commit id (Alias (oid,aast)); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok +let allow_nested_proofs = ref false +let _ = Goptions.declare_bool_option + { Goptions.optdepr = false; + Goptions.optname = "Nested Proofs Allowed"; + Goptions.optkey = ["Nested";"Proofs";"Allowed"]; + Goptions.optread = (fun () -> !allow_nested_proofs); + Goptions.optwrite = (fun b -> allow_nested_proofs := b) } + let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); @@ -2802,6 +2810,15 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) (* Proof *) | VtStartProof (mode, guarantee, names), w -> + + if not !allow_nested_proofs && VCS.proof_nesting () > 0 then + "Nested proofs are not allowed 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 bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; -- cgit v1.2.3