Closed bugs.

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v
new file mode 100644
index 000000000..9eeb86468
--- /dev/null
+++ b/test-suite/bugs/closed/4433.v
@@ -0,0 +1,29 @@
+Require Import Coq.Arith.Arith Coq.Init.Wf.
+Axiom proof_admitted : False.
+Goal exists x y z : nat, Fix
+                           Wf_nat.lt_wf
+                           (fun _ => nat -> nat)
+                           (fun x' f => match x' as x'0
+                                              return match x'0 with
+                                                       | 0 => True
+                                                       | S x'' => x'' < x'
+                                                     end
+                                                     -> nat -> nat
+                                        with
+                                          | 0 => fun _ _ => 0
+                                          | S x'' => f x''
+                                        end
+                                          (match x' with
+                                             | 0 => I
+                                             | S x'' => (Nat.lt_succ_diag_r _)
+                                           end))
+                           z
+                           y
+                         = 0.
+Proof.
+  do 3 (eexists; [ shelve.. | ]).
+  match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end.
+  case proof_admitted.
+  Unshelve.
+  all:constructor.
+Defined.
\ No newline at end of file