diff options
| author | Maxime Dénès | 2018-12-07 13:59:15 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:45:35 +0200 |
| commit | f5d41cecf9bbdef785b5370b8fdec7afa8563fc4 (patch) | |
| tree | 558fcd6910a8075c0c27c31e953243433f733803 /test-suite/success/ProgramWf.v | |
| parent | 4c148ecfd85e6df2edf544d3ed9079c36ed1ba39 (diff) | |
Fix spurious argument of {measure}
Previsouly, it was silently ignored.
Diffstat (limited to 'test-suite/success/ProgramWf.v')
| -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 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 := _. |