From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/bugs/closed/3481.v | 70 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)
 create mode 100644 test-suite/bugs/closed/3481.v

(limited to 'test-suite/bugs/closed/3481.v')

diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v
new file mode 100644
index 00000000..89d476dc
--- /dev/null
+++ b/test-suite/bugs/closed/3481.v
@@ -0,0 +1,70 @@
+
+Set Implicit Arguments.
+
+Require Import Logic.
+Module NonPrim.
+Local Set Record Elimination Schemes.
+Record prodwithlet (A B : Type) : Type :=
+  pair' { fst : A; fst' := fst; snd : B }.
+
+Definition letreclet (p : prodwithlet nat nat) :=
+  let (x, x', y) := p in x + y.
+
+Definition pletreclet (p : prodwithlet nat nat) :=
+  let 'pair' x x' y := p in x + y + x'.
+
+Definition pletreclet2 (p : prodwithlet nat nat) :=
+  let 'pair' x y := p in x + y.
+
+Check (pair 0 0).
+End NonPrim.
+
+Global Set Universe Polymorphism.
+Global Set Asymmetric Patterns.
+Local Set Record Elimination Schemes.
+Local Set Primitive Projections.
+
+Record prod (A B : Type) : Type :=
+  pair { fst : A; snd : B }.
+
+Print prod_rect.
+
+(* What I really want: *)
+Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B), P (pair fst snd))
+           (p : prod A B) : P p
+  := u (fst p) (snd p).
+
+Definition conv : @prod_rect = @prod_rect'.
+Proof. reflexivity. Defined.
+
+Definition imposs :=
+  (fun A B P f (p : prod A B) => match p as p0 return P p0 with
+                                   | {| fst := x ; snd := x0 |} => f x x0
+                                 end).
+
+Definition letrec (p : prod nat nat) :=
+  let (x, y) := p in x + y.
+Eval compute in letrec (pair 1 5).
+
+Goal forall p : prod nat nat, letrec p = fst p + snd p.
+Proof.
+  reflexivity.
+  Undo.
+  intros p.
+  case p. simpl. unfold letrec. simpl. reflexivity.
+Defined.
+
+Eval compute in conv. (* = eq_refl
+     : prod_rect = prod_rect' *)
+
+Check eq_refl : @prod_rect = @prod_rect'. (* Toplevel input, characters 6-13:
+Error:
+The term "eq_refl" has type "prod_rect = prod_rect"
+while it is expected to have type "prod_rect = prod_rect'"
+(cannot unify "prod_rect" and "prod_rect'"). *)
+
+Record sigma (A : Type) (B : A -> Type) : Type :=
+  dpair { pi1 : A ; pi2 : B pi1 }.
+
+
+
-- 
cgit v1.2.3