From c5194d098dce2ab829b63afde4199b750ea85e31 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 2 Jul 2014 10:55:05 +0200 Subject: Indeed simpl never is really honored now. --- test-suite/bugs/closed/3322.v | 23 +++++++++++++++++++++++ test-suite/bugs/opened/3322.v | 23 ----------------------- 2 files changed, 23 insertions(+), 23 deletions(-) create mode 100644 test-suite/bugs/closed/3322.v delete mode 100644 test-suite/bugs/opened/3322.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/3322.v b/test-suite/bugs/closed/3322.v new file mode 100644 index 000000000..925f22a21 --- /dev/null +++ b/test-suite/bugs/closed/3322.v @@ -0,0 +1,23 @@ +(* File reduced by coq-bug-finder from original input, then from 11971 lines to 11753 lines, then from 7702 lines to 564 lines, then from 571 lines to 61 lines *) +Set Asymmetric Patterns. +Axiom admit : forall {T}, T. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. +Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (pq : {p : (projT1 u) = (projT1 v) & transport _ p (projT2 u) = (projT2 v)}) +: u = v. +Proof. + destruct pq as [p q], u as [x y], v as [x' y']; simpl in *. + destruct p, q; simpl; reflexivity. +Defined. +Arguments path_sigma_uncurried : simpl never. +Section opposite. + Let opposite_functor_involutive_helper + := @path_sigma_uncurried admit admit (existT _ admit admit) admit (existT _ admit admit). + + Goal True. + Opaque path_sigma_uncurried. + simpl in *. + Transparent path_sigma_uncurried. + (* This command should fail with "Error: Failed to progress.", as it does in 8.4; the simpl never directive should prevent simpl from progressing *) + Fail progress simpl in *. diff --git a/test-suite/bugs/opened/3322.v b/test-suite/bugs/opened/3322.v deleted file mode 100644 index 67a68d55e..000000000 --- a/test-suite/bugs/opened/3322.v +++ /dev/null @@ -1,23 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 11971 lines to 11753 lines, then from 7702 lines to 564 lines, then from 571 lines to 61 lines *) -Set Asymmetric Patterns. -Axiom admit : forall {T}, T. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. -Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) - (pq : {p : (projT1 u) = (projT1 v) & transport _ p (projT2 u) = (projT2 v)}) -: u = v. -Proof. - destruct pq as [p q], u as [x y], v as [x' y']; simpl in *. - destruct p, q; simpl; reflexivity. -Defined. -Arguments path_sigma_uncurried : simpl never. -Section opposite. - Let opposite_functor_involutive_helper - := @path_sigma_uncurried admit admit (existT _ admit admit) admit (existT _ admit admit). - - Goal True. - Opaque path_sigma_uncurried. - simpl in *. - Transparent path_sigma_uncurried. - (* This command should fail with "Error: Failed to progress.", as it does in 8.4; the simpl never directive should prevent simpl from progressing *) - progress simpl in *. -- cgit v1.2.3