diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-28 13:47:39 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-28 13:47:39 +0200 |
commit | 3bdadb4020c1d3e51957a06c1e3a52744f09148d (patch) | |
tree | 4236eaa3d1858de16882223fd2eabeb30216c44d /test-suite/bugs/opened | |
parent | 86e2b0ab9da7dbd9c4c39ab2ab8df05d94a42056 (diff) |
Tests for bugs #3509 and #3510.
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r-- | test-suite/bugs/opened/3509.v | 19 | ||||
-rw-r--r-- | test-suite/bugs/opened/3510.v | 35 |
2 files changed, 0 insertions, 54 deletions
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v deleted file mode 100644 index 3913bbb43..000000000 --- a/test-suite/bugs/opened/3509.v +++ /dev/null @@ -1,19 +0,0 @@ -Require Import TestSuite.admit. -Lemma match_bool_fn b A B xT xF -: match b as b return forall x : A, B b x with - | true => xT - | false => xF - end - = fun x : A => match b as b return B b x with - | true => xT x - | false => xF x - end. -admit. -Defined. -Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f -: (if b as b return B (if b then t else f) then F t else F f) - = F (if b then t else f). -admit. -Defined. -Hint Rewrite match_bool_fn : matchdb. -Fail Hint Rewrite match_bool_comm_1 : matchdb. diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v deleted file mode 100644 index daf265071..000000000 --- a/test-suite/bugs/opened/3510.v +++ /dev/null @@ -1,35 +0,0 @@ -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. |