From 7012d65f71752a89cded69d6c2e7045f3a7cadde Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 27 Feb 2015 13:29:11 +0100 Subject: Moving tests for #2456 and #3593 to "opened" until they're fixed. --- test-suite/bugs/closed/2456.v | 53 ------------------------------------------- test-suite/bugs/closed/3593.v | 10 -------- test-suite/bugs/opened/2456.v | 53 +++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/3593.v | 10 ++++++++ 4 files changed, 63 insertions(+), 63 deletions(-) delete mode 100644 test-suite/bugs/closed/2456.v delete mode 100644 test-suite/bugs/closed/3593.v create mode 100644 test-suite/bugs/opened/2456.v create mode 100644 test-suite/bugs/opened/3593.v diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v deleted file mode 100644 index 56f046c4d7..0000000000 --- a/test-suite/bugs/closed/2456.v +++ /dev/null @@ -1,53 +0,0 @@ - -Require Import Equality. - -Parameter Patch : nat -> nat -> Set. - -Inductive Catch (from to : nat) : Type - := MkCatch : forall (p : Patch from to), - Catch from to. -Implicit Arguments MkCatch [from to]. - -Inductive CatchCommute5 - : forall {from mid1 mid2 to : nat}, - Catch from mid1 - -> Catch mid1 to - -> Catch from mid2 - -> Catch mid2 to - -> Prop - := MkCatchCommute5 : - forall {from mid1 mid2 to : nat} - (p : Patch from mid1) - (q : Patch mid1 to) - (q' : Patch from mid2) - (p' : Patch mid2 to), - CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p'). - -Inductive CatchCommute {from mid1 mid2 to : nat} - (p : Catch from mid1) - (q : Catch mid1 to) - (q' : Catch from mid2) - (p' : Catch mid2 to) - : Prop - := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'), - CatchCommute p q q' p'. -Notation "<< p , q >> <~> << q' , p' >>" - := (CatchCommute p q q' p') - (at level 60, no associativity). - -Lemma CatchCommuteUnique2 : - forall {from mid mid' to : nat} - {p : Catch from mid} {q : Catch mid to} - {q' : Catch from mid'} {p' : Catch mid' to} - {q'' : Catch from mid'} {p'' : Catch mid' to} - (commute1 : <> <~> <>) - (commute2 : <> <~> <>), - (p' = p'') /\ (q' = q''). -Proof with auto. -intros. -set (X := commute2). -dependent destruction commute1; -dependent destruction catchCommuteDetails; -dependent destruction commute2; -dependent destruction catchCommuteDetails generalizing X. -Admitted. \ No newline at end of file diff --git a/test-suite/bugs/closed/3593.v b/test-suite/bugs/closed/3593.v deleted file mode 100644 index 25f9db6b28..0000000000 --- a/test-suite/bugs/closed/3593.v +++ /dev/null @@ -1,10 +0,0 @@ -Set Universe Polymorphism. -Set Printing All. -Set Implicit Arguments. -Record prod A B := pair { fst : A ; snd : B }. -Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. -simpl; intros. - constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). - Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). - reflexivity. -Qed. diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v new file mode 100644 index 0000000000..56f046c4d7 --- /dev/null +++ b/test-suite/bugs/opened/2456.v @@ -0,0 +1,53 @@ + +Require Import Equality. + +Parameter Patch : nat -> nat -> Set. + +Inductive Catch (from to : nat) : Type + := MkCatch : forall (p : Patch from to), + Catch from to. +Implicit Arguments MkCatch [from to]. + +Inductive CatchCommute5 + : forall {from mid1 mid2 to : nat}, + Catch from mid1 + -> Catch mid1 to + -> Catch from mid2 + -> Catch mid2 to + -> Prop + := MkCatchCommute5 : + forall {from mid1 mid2 to : nat} + (p : Patch from mid1) + (q : Patch mid1 to) + (q' : Patch from mid2) + (p' : Patch mid2 to), + CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p'). + +Inductive CatchCommute {from mid1 mid2 to : nat} + (p : Catch from mid1) + (q : Catch mid1 to) + (q' : Catch from mid2) + (p' : Catch mid2 to) + : Prop + := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'), + CatchCommute p q q' p'. +Notation "<< p , q >> <~> << q' , p' >>" + := (CatchCommute p q q' p') + (at level 60, no associativity). + +Lemma CatchCommuteUnique2 : + forall {from mid mid' to : nat} + {p : Catch from mid} {q : Catch mid to} + {q' : Catch from mid'} {p' : Catch mid' to} + {q'' : Catch from mid'} {p'' : Catch mid' to} + (commute1 : <> <~> <>) + (commute2 : <> <~> <>), + (p' = p'') /\ (q' = q''). +Proof with auto. +intros. +set (X := commute2). +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails generalizing X. +Admitted. \ No newline at end of file diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v new file mode 100644 index 0000000000..25f9db6b28 --- /dev/null +++ b/test-suite/bugs/opened/3593.v @@ -0,0 +1,10 @@ +Set Universe Polymorphism. +Set Printing All. +Set Implicit Arguments. +Record prod A B := pair { fst : A ; snd : B }. +Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. +simpl; intros. + constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). + Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + reflexivity. +Qed. -- cgit v1.2.3