diff options
| author | Maxime Dénès | 2018-12-07 13:58:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:45:35 +0200 |
| commit | 4c148ecfd85e6df2edf544d3ed9079c36ed1ba39 (patch) | |
| tree | 824a4ff8290d2d9bf5f584ca4a84dd29d4c9fcf2 | |
| parent | 414cfd64702be920c9d96514e3802bc950b5ea0b (diff) | |
Take advantage of relaxed {measure} syntax in test suite
| -rw-r--r-- | test-suite/success/ProgramWf.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 |