diff options
Diffstat (limited to 'test-suite/success/ProgramWf.v')
| -rw-r--r-- | test-suite/success/ProgramWf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 3b7f0d84..681c4716 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -100,6 +100,6 @@ Next Obligation. simpl in *; intros. apply H. simpl. omega. Qed. -Program Fixpoint check_n' (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p) +Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) {measure (p - n) p} : nat := - _. + _.
\ No newline at end of file |