diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:19:16 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:19:16 +0200 |
commit | 82dc05efc11514c2c05ec17e448e0b4b322e7c86 (patch) | |
tree | 02c45297dacfa632a9926dceb514c8ee3ef50cdd /test-suite/bugs | |
parent | 51555af3cccae1f73bfe97e4347a5c625c6d0ec6 (diff) | |
parent | 2c7fb44684b26d9c9aea0794b9f0d52088337477 (diff) |
Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of tactic unification.
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/7011.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v new file mode 100644 index 000000000..296e4e11e --- /dev/null +++ b/test-suite/bugs/closed/7011.v @@ -0,0 +1,16 @@ +(* Fix and Cofix were missing in tactic unification *) + +Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end) + = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end). +Proof. + eexists. + reflexivity. +Qed. + +CoInductive stream := cons : nat -> stream -> stream. + +Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo). +Proof. + eexists. + reflexivity. +Qed. |