From 49d73185be33ce521f4664e61d47b2db5d59d608 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?=
 <theo.zimmermann@univ-paris-diderot.fr>
Date: Thu, 10 May 2018 10:16:14 +0200
Subject: [PATCH 1/4] Introduce an option to allow nested lemma, and turn it
 off by default.

---
 stm/stm.ml                       | 17 +++++++++++++++++
 test-suite/bugs/closed/2969.v    |  2 ++
 test-suite/bugs/closed/3377.v    |  3 ++-
 test-suite/bugs/closed/4069.v    |  2 ++
 test-suite/bugs/closed/4198.v    |  2 ++
 test-suite/bugs/closed/4782.v    |  2 ++
 test-suite/ide/undo012.fake      |  1 +
 test-suite/ide/undo013.fake      |  1 +
 test-suite/ide/undo014.fake      |  1 +
 test-suite/ide/undo015.fake      |  1 +
 test-suite/ide/undo016.fake      |  1 +
 test-suite/output/Cases.v        |  1 +
 test-suite/output/ltac.v         |  3 +++
 test-suite/success/Inversion.v   |  2 ++
 test-suite/success/RecTutorial.v |  2 ++
 test-suite/success/destruct.v    |  1 +
 test-suite/success/refine.v      |  4 +++-
 test-suite/success/sideff.v      |  2 ++
 18 files changed, 46 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 9ea6a305efec..90360dce9cb6 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;
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index a03adbd73c12..7b1a2617899f 100644
--- a/test-suite/bugs/closed/2969.v
+++ b/test-suite/bugs/closed/2969.v
@@ -12,6 +12,7 @@ eexists.
 reflexivity.
 Grab Existential Variables.
 admit.
+Admitted.
 
 (* Alternative variant which failed but without raising anomaly *)
 
@@ -24,3 +25,4 @@ clearbody n n0.
 exact I.
 Grab Existential Variables.
 admit.
+Admitted.
diff --git a/test-suite/bugs/closed/3377.v b/test-suite/bugs/closed/3377.v
index 8e9e3933cc76..abfcf1d35593 100644
--- a/test-suite/bugs/closed/3377.v
+++ b/test-suite/bugs/closed/3377.v
@@ -5,6 +5,7 @@ Record prod A B := pair { fst : A; snd : B}.
 Goal fst (@pair Type Type Type Type).
 Set Printing All.
 match goal with |- ?f ?x => set (foo := f x) end.
+Abort.
 
 Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x).
 Proof.
@@ -12,6 +13,6 @@ Proof.
   lazymatch goal with
     | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f
   end.
-
 (* Toplevel input, characters 7-44:
 Error: No matching clauses for match. *)
+Abort.
diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v
index 606c6e084530..668f6bb428b7 100644
--- a/test-suite/bugs/closed/4069.v
+++ b/test-suite/bugs/closed/4069.v
@@ -41,6 +41,8 @@ Proof. f_equal.
   8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l
     and skipn n l = l
 *)
+Abort.
+
 Require Import List.
 Fixpoint replicate {A} (n : nat) (x : A) : list A :=
   match n with 0 => nil | S n => x :: replicate n x end.
diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v
index eb37141bcfb8..28800ac05ac2 100644
--- a/test-suite/bugs/closed/4198.v
+++ b/test-suite/bugs/closed/4198.v
@@ -13,6 +13,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'),
   match goal with
     | [ |- context G[@hd] ] => idtac
   end.
+Abort.
 
 (* This second example comes from CFGV where inspecting subterms of a
    match is expecting to inspect first the term to match (even though
@@ -35,3 +36,4 @@ Ltac mydestruct :=
 Goal forall x, match x with 0 => 0 | _ => 0 end = 0.
 intros.
 mydestruct.
+Abort.
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index dbd71035dc64..1e1a4cb9c29d 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -6,6 +6,7 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
+Abort.
  
 (* A simplification of an example from coquelicot, which was failing
    at some time after a fix #4782 was committed. *)
@@ -21,4 +22,5 @@ Set Typeclasses Debug.
 Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
 intros.
 apply (F _ _)  with (x,x).
+Abort.
   
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
index b3d1c6d534b0..c95df1b11c94 100644
--- a/test-suite/ide/undo012.fake
+++ b/test-suite/ide/undo012.fake
@@ -3,6 +3,7 @@
 #
 # Test backtracking in presence of nested proofs
 #
+ADD { Set Nested Proofs Allowed. }
 ADD { Lemma aa : True -> True /\ True. }
 ADD { intro H. }
 ADD { split. }
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index 921a9d0f0d67..a3ccefd2ca00 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -4,6 +4,7 @@
 # Test backtracking in presence of nested proofs
 # Second, trigger the undo of an inner proof
 #
+ADD { Set Nested Proofs Allowed. }
 ADD { Lemma aa : True -> True /\ True. }
 ADD { intro H. }
 ADD { split. }
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
index f5fe774704bb..13e718229c98 100644
--- a/test-suite/ide/undo014.fake
+++ b/test-suite/ide/undo014.fake
@@ -4,6 +4,7 @@
 # Test backtracking in presence of nested proofs
 # Third, undo inside an inner proof
 #
+ADD { Set Nested Proofs Allowed. }
 ADD { Lemma aa : True -> True /\ True. }
 ADD { intro H. }
 ADD { split. }
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
index a1e5c947b3ce..9cbd64460dda 100644
--- a/test-suite/ide/undo015.fake
+++ b/test-suite/ide/undo015.fake
@@ -4,6 +4,7 @@
 # Test backtracking in presence of nested proofs
 # Fourth, undo from an inner proof to a above proof
 #
+ADD { Set Nested Proofs Allowed. }
 ADD { Lemma aa : True -> True /\ True. }
 ADD { intro H. }
 ADD { split. }
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index f9414c1ea7a3..15bd3cc92d61 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -4,6 +4,7 @@
 # Test backtracking in presence of nested proofs
 # Fifth, undo from an inner proof to a previous inner proof
 #
+ADD { Set Nested Proofs Allowed. }
 ADD { Lemma aa : True -> True /\ True. }
 ADD { intro H. }
 ADD { split. }
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index caf3b28701b9..4740c009a489 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -163,6 +163,7 @@ match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end)
 match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
 match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
 Show.
+Abort.
 
 Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
 let y := fresh "n" in (* Checking that y is hidden *)
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 6adbe95dd511..901b1e3aa6e4 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -37,17 +37,20 @@ Fail g1 I.
 Fail f1 I.
 Fail g2 I.
 Fail f2 I.
+Abort.
 
 Ltac h x := injection x.
 Goal True -> False.
 Fail h I.
 intro H.
 Fail h H.
+Abort.
 
 (* Check printing of the "var" argument "Hx" *)
 Ltac m H := idtac H; exact H.
 Goal True.
 let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+Abort.
 
 (* Check consistency of interpretation scopes (#4398) *)
 
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index ca8da394829f..ee540d71099d 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -107,6 +107,7 @@ Goal forall o, foo2 o -> 0 = 1.
 intros.
 eapply trans_eq.
 inversion H.
+Abort.
 
 (* Check that the part of "injection" that is called by "inversion"
    does the same number of intros as the number of equations
@@ -136,6 +137,7 @@ Goal True -> True.
 intro.
 Fail inversion H using False.
 Fail inversion foo using True_ind.
+Abort.
 
 (* Was failing at some time between 7 and 10 September 2014 *)
 (* even though, it is not clear that the resulting context is interesting *)
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 29350d620e0f..6370cab6b2ae 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -589,6 +589,8 @@ Close Scope Z_scope.
 
 Theorem S_is_not_O : forall n, S n <> 0.
 
+Set Nested Proofs Allowed.
+
 Definition Is_zero (x:nat):= match x with
                                      | 0 => True
                                      | _ => False
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 6fbe61a9befa..d1d384659b82 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -422,6 +422,7 @@ Abort.
 Goal forall b:bool, b = b.
 intros.
 destruct b eqn:H.
+Abort.
 
 (* Check natural instantiation behavior when the goal has already an evar *)
 
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 22fb4d7576a6..40986e57cb82 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -121,14 +121,16 @@ Abort.
 (* Wish 1988: that fun forces unfold in refine *)
 
 Goal (forall A : Prop, A -> ~~A).
-Proof. refine(fun A a f => _).
+Proof. refine(fun A a f => _). Abort.
 
 (* Checking beta-iota normalization of hypotheses in created evars *)
 
 Goal {x|x=0} -> True.
 refine (fun y => let (x,a) := y in _).
 match goal with a:_=0 |- _ => idtac end.
+Abort.
 
 Goal (forall P, {P 0}+{P 1}) -> True.
 refine (fun H => if H (fun x => x=x) then _ else _).
 match goal with _:0=0 |- _ => idtac end.
+Abort.
diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v
index 3c0b81568afb..b9a1273b1a97 100644
--- a/test-suite/success/sideff.v
+++ b/test-suite/success/sideff.v
@@ -5,6 +5,8 @@ Proof.
   apply (const tt tt).
 Qed.
 
+Set Nested Proofs Allowed.
+
 Lemma foobar' : unit.
   Lemma aux : forall A : Type, A -> unit.
   Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.

From 1ffa181c8015584fe1762a5ab8f6a664725767fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?=
 <theo.zimmermann@univ-paris-diderot.fr>
Date: Wed, 9 May 2018 17:48:44 +0200
Subject: [PATCH 2/4] Remove deprecation warning for nested proofs.

It is not clear yet that support for nested proofs will actually get removed in a future version.
---
 stm/stm.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 90360dce9cb6..9192c141027a 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

From 17a2ba8d59c9b459bb67a09cb0374ca9a1eea634 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 11 May 2018 10:19:35 +0200
Subject: [PATCH 3/4] [STM] Nested Proofs Allowed has to be executed
 immediately

since it affects scheduling (actually the error the option lets one
silence)
---
 stm/stm.ml                | 2 +-
 stm/vernac_classifier.ml  | 9 ++++++++-
 stm/vernac_classifier.mli | 1 +
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 9192c141027a..20409c25ee11 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2768,7 +2768,7 @@ 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.optkey   = Vernac_classifier.stm_allow_nested_proofs_option_name;
       Goptions.optread  = (fun () -> !allow_nested_proofs);
       Goptions.optwrite = (fun b -> allow_nested_proofs := b) }
 
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c08cc6e36737..e01dcbcb6e8a 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 abbc04e895eb..45fbfb42af73 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

From c9b4073104385f6079f260c5183bb3a6a989b7d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?=
 <theo.zimmermann@univ-paris-diderot.fr>
Date: Tue, 15 May 2018 11:30:24 +0200
Subject: [PATCH 4/4] Document nested proofs and associated option.

---
 CHANGES                                             |  3 +++
 .../language/gallina-specification-language.rst     |  3 ++-
 doc/sphinx/proof-engine/proof-handling.rst          | 13 +++++++++++++
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index cdc1ff6a635d..3030e3311c2f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,9 @@ Vernacular Commands
 
 - Removed deprecated commands Arguments Scope and Implicit Arguments
   (not the option). Use the Arguments command instead.
+- Nested proofs may be enabled through the option `Nested Proofs Allowed`.
+  By default, they are disabled and produce an error. The deprecation
+  warning which used to occur when using nested proofs has been removed.
 
 Tactics
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 4dcd7deb13a5..d17043105897 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1339,7 +1339,8 @@ using the keyword :cmd:`Qed`.
 
 .. note::
 
-   #. Several statements can be simultaneously asserted.
+   #. Several statements can be simultaneously asserted provided option
+      :opt:`Nested Proofs Allowed` was turned on.
 
    #. Not only other assertions but any vernacular command can be given
       while in the process of proving a given assertion. In this case, the
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 6d0b27728105..eba0db3ff5d1 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -113,6 +113,8 @@ list of assertion commands is given in :ref:`Assertions`. The command
       Aborts the editing of the proof named :token:`ident` (in case you have
       nested proofs).
 
+      .. seealso:: :opt:`Nested Proofs Allowed`
+
    .. cmdv:: Abort All
 
       Aborts all current goals.
@@ -561,6 +563,17 @@ Controlling the effect of proof editing commands
    has to be used to move the assumptions to the local context.
 
 
+.. opt:: Nested Proofs Allowed
+
+   When turned on (it is off by default), this option enables support for nested
+   proofs: a new assertion command can be inserted before the current proof is
+   finished, in which case Coq will temporarily switch to the proof of this
+   *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
+   or :cmd:`Defined`), its statement will be made available (as if it had been
+   proved before starting the previous proof) and Coq will switch back to the
+   proof of the previous assertion.
+
+
 Controlling memory usage
 ------------------------