From 51b4d0cdad77f2874bd481dabd32e0772563dc3f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 3 Mar 2015 15:47:24 +0100 Subject: Fix bug #4103: forgot to allow unfolding projections of cofixpoints like cases, in some cases. --- test-suite/bugs/closed/4103.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 test-suite/bugs/closed/4103.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v new file mode 100644 index 000000000..92cc0279a --- /dev/null +++ b/test-suite/bugs/closed/4103.v @@ -0,0 +1,12 @@ +Set Primitive Projections. + +CoInductive stream A := { hd : A; tl : stream A }. + +CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}. + +Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _). +Proof. + eexists. + (* Set Debug Tactic Unification. *) + (* Set Debug RAKAM. *) + reflexivity. -- cgit v1.2.3