From 0f1814bcbaafbd93d7c7587eef8826a80b65477f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 17:52:19 +0200
Subject: [function] always open a proof when used with `wf` or `measure`

---
 test-suite/bugs/closed/bug_1618.v | 1 +
 test-suite/bugs/closed/bug_4306.v | 2 ++
 2 files changed, 3 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_1618.v b/test-suite/bugs/closed/bug_1618.v
index a7be12e26f..041055a38f 100644
--- a/test-suite/bugs/closed/bug_1618.v
+++ b/test-suite/bugs/closed/bug_1618.v
@@ -20,3 +20,4 @@ a :=
   match a return (P a) with
     | A1 n => f n
   end.
+Proof. Defined.
diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v
index 80c348d207..f1bce04451 100644
--- a/test-suite/bugs/closed/bug_4306.v
+++ b/test-suite/bugs/closed/bug_4306.v
@@ -30,3 +30,5 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
                                 | Gt => y :: foo (xs, ys')
                               end
   end.
+Proof.
+Defined.
-- 
cgit v1.2.3