aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--stm/stm.ml17
-rw-r--r--test-suite/bugs/closed/2969.v2
-rw-r--r--test-suite/bugs/closed/3377.v3
-rw-r--r--test-suite/bugs/closed/4069.v2
-rw-r--r--test-suite/bugs/closed/4198.v2
-rw-r--r--test-suite/bugs/closed/4782.v2
-rw-r--r--test-suite/ide/undo012.fake1
-rw-r--r--test-suite/ide/undo013.fake1
-rw-r--r--test-suite/ide/undo014.fake1
-rw-r--r--test-suite/ide/undo015.fake1
-rw-r--r--test-suite/ide/undo016.fake1
-rw-r--r--test-suite/output/Cases.v1
-rw-r--r--test-suite/output/ltac.v3
-rw-r--r--test-suite/success/Inversion.v2
-rw-r--r--test-suite/success/RecTutorial.v2
-rw-r--r--test-suite/success/destruct.v1
-rw-r--r--test-suite/success/refine.v4
-rw-r--r--test-suite/success/sideff.v2
18 files changed, 46 insertions, 2 deletions
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;
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 10:33:10 +0000