aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3481.v
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-04 00:39:49 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-04 01:13:33 +0200
commitcd10b70637dea3cbba5785d163bc567a32a031a8 (patch)
tree046d26c33c0b9a0a58bdf6d0d56c5e5dcaf919cd /test-suite/bugs/closed/3481.v
parent593dfd66a5016ba457b6dccf1179a0e1ec7bff84 (diff)
Add test suite files for closed bugs.
Diffstat (limited to 'test-suite/bugs/closed/3481.v')
-rw-r--r--test-suite/bugs/closed/3481.v70
1 files changed, 70 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v
new file mode 100644
index 000000000..1f180cd94
--- /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.
+
+Fail 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 }.
+
+
+