aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-07-28 13:57:00 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-07-28 13:57:00 +0200
commit309907165909a08c4b6c2c05e87f458bb1873f91 (patch)
tree79a64fa5270794e837ce6578216773739bd1d996 /test-suite/bugs
parent3bdadb4020c1d3e51957a06c1e3a52744f09148d (diff)
Updating test-suite for #3510.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/3510.v40
1 files changed, 5 insertions, 35 deletions
diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
index daf265071..4cbae3359 100644
--- a/test-suite/bugs/closed/3510.v
+++ b/test-suite/bugs/closed/3510.v
@@ -1,35 +1,5 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
- | Some k => s k
- | None => n
- end
- = fun x : A => match b as b return B b x with
- | Some k => s k x
- | None => n x
- end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
- | Some k => s1 k
- | None => n1
- end
- match p as p return B match p with Some k => s1 k | None => n1 end with
- | Some k => s2 k
- | None => n2
- end with
- | Some k => f (s1 k) (s2 k)
- | None => f n1 n2
- end
- = f match p return A with
- | Some k => s1 k
- | None => n1
- end
- match p as p return B match p with Some k => s1 k | None => n1 end with
- | Some k => s2 k
- | None => n2
- end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 a2 : bar.