Add test-suite files for closed bugs.

1 files changed, 32 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v
new file mode 100644
index 000000000..33ca9651a
--- /dev/null
+++ b/test-suite/bugs/closed/3783.v
@@ -0,0 +1,32 @@
+Fixpoint exp (n : nat) (T : Set)
+  := match n with
+       | 0 => T
+       | S n' => exp n' (T * T)
+     end.
+Definition big := Eval compute in exp 13 nat.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Time cbv beta in y. (* 0s *)
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Timeout 1 cbv beta in y. (* takes around 2s.  Grows with the value passed to [exp] above *)
+    admit.
+  Defined.
+End Prim.
\ No newline at end of file