Introduce an option to allow nested lemma, and turn it off by default.

5 files changed, 10 insertions, 1 deletions

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.