From eff360695af18476bfca0edfdea467cbf9203984 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Dec 2019 20:57:01 +0100
Subject: Unfortunate bug with "cofix with": case of a CProdN over no bindings.

Failing on CProdN([],...) was maybe a bit too radical.
---
 test-suite/success/RecTutorial.v |  4 ----
 test-suite/success/cofixtac.v    | 10 ++++++++++
 2 files changed, 10 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/success/cofixtac.v

(limited to 'test-suite')

diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 6370cab6b2..4fac798f76 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1210,7 +1210,3 @@ Proof.
  constructor.
  trivial.
 Qed.
-
-
-
-
diff --git a/test-suite/success/cofixtac.v b/test-suite/success/cofixtac.v
new file mode 100644
index 0000000000..ae75ee770f
--- /dev/null
+++ b/test-suite/success/cofixtac.v
@@ -0,0 +1,10 @@
+CoInductive stream :=
+| C : content -> stream
+with content :=
+| D : nat -> stream -> content.
+
+Lemma one : stream.
+cofix c with (d : content).
+- constructor. apply d.
+- constructor. exact 1. apply c.
+Defined.
-- 
cgit v1.2.3