Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by default.

3 files changed, 27 insertions, 9 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 9ea6a305ef..20409c25ee 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2113,12 +2113,6 @@ let delegate name =
   || VCS.is_vio_doc ()
   || !cur_opt.async_proofs_full
 
-let warn_deprecated_nested_proofs =
-  CWarnings.create ~name:"deprecated-nested-proofs" ~category:"deprecated"
-         (fun () ->
-          strbrk ("Nested proofs are deprecated and will "^
-                    "stop working in a future Coq version"))
-
 let collect_proof keep cur hd brkind id =
  stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
@@ -2200,8 +2194,7 @@ let collect_proof keep cur hd brkind id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
         `MaybeASync (parent last, accn, name, delegate name)
-    | `Sideff _ ->
-       warn_deprecated_nested_proofs ();
+    | `Sideff (CherryPickEnv,_) ->
         `Sync (no_name,`NestedProof)
     | _ -> `Sync (no_name,`Unknown) in
  let make_sync why = function
@@ -2771,6 +2764,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   = Vernac_classifier.stm_allow_nested_proofs_option_name;
+      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 +2803,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;
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c08cc6e367..e01dcbcb6e 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -54,13 +54,20 @@ let idents_of_name : Names.Name.t -> Names.Id.t list =
   | Names.Anonymous -> []
   | Names.Name n -> [n]
 
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+  [ Vernacentries.universe_polymorphism_option_name;
+    stm_allow_nested_proofs_option_name ]
+
 let classify_vernac e =
   let static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
     | ( VernacSetOption (_, l,_) | VernacUnsetOption (_, l))
-      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+      when CList.exists (CList.equal String.equal l)
+        options_affecting_stm_scheduling ->
        VtSideff [], VtNow
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index abbc04e895..45fbfb42af 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -25,3 +25,4 @@ val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
 val classify_as_proofstep : vernac_classification
 
+val stm_allow_nested_proofs_option_name : string list