diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1604.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1604.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v deleted file mode 100644 index 22c3df82..00000000 --- a/test-suite/bugs/closed/shouldsucceed/1604.v +++ /dev/null @@ -1,7 +0,0 @@ -Require Import Setoid. - -Parameter F : nat -> nat. -Axiom F_id : forall n : nat, n = F n. -Goal forall n : nat, F n = n. -intro n. setoid_rewrite F_id at 3. reflexivity. -Qed. |