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

23 files changed, 74 insertions, 12 deletions

diff --git a/CHANGES b/CHANGES
index cdc1ff6a6..3030e3311 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 4dcd7deb1..d17043105 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 6d0b27728..eba0db3ff 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
 ------------------------
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 9ea6a305e..20409c25e 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 c08cc6e36..e01dcbcb6 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 abbc04e89..45fbfb42a 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
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index a03adbd73..7b1a26178 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 8e9e3933c..abfcf1d35 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 606c6e084..668f6bb42 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 eb37141bc..28800ac05 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 dbd71035d..1e1a4cb9c 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 b3d1c6d53..c95df1b11 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 921a9d0f0..a3ccefd2c 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 f5fe77470..13e718229 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 a1e5c947b..9cbd64460 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 f9414c1ea..15bd3cc92 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 caf3b2870..4740c009a 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 6adbe95dd..901b1e3aa 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 ca8da3948..ee540d710 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 29350d620..6370cab6b 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 6fbe61a9b..d1d384659 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 22fb4d757..40986e57c 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 3c0b81568..b9a1273b1 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.