From 4c148ecfd85e6df2edf544d3ed9079c36ed1ba39 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 7 Dec 2018 13:58:12 +0100
Subject: Take advantage of relaxed {measure} syntax in test suite

---
 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 85d7a770fc..0c4fa31311 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -13,7 +13,7 @@ Print sigT_rect.
 Obligation Tactic := program_simplify ; auto with *.
 About MR.
 
-Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
+Program Fixpoint merge (n m : nat) {measure (n + m) lt} : nat :=
   match n with
     | 0 => 0
     | S n' => merge n' m
-- 
cgit v1.2.3