From f5d41cecf9bbdef785b5370b8fdec7afa8563fc4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 7 Dec 2018 13:59:15 +0100
Subject: Fix spurious argument of {measure}

Previsouly, it was silently ignored.
---
 test-suite/success/ProgramWf.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 0c4fa31311..02adb012d9 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -101,5 +101,5 @@ Next Obligation. simpl in *; intros.
 Qed.
 
 Program Fixpoint check_n'  (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p})
-  {measure (p - n) p} : nat :=
+  {measure (p - n)} : nat :=
   _.
-- 
cgit v1.2.3