diff options
Diffstat (limited to 'test-suite/success/ProgramWf.v')
| -rw-r--r-- | test-suite/success/ProgramWf.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 18111f07c5..81bdbc29f0 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -56,7 +56,10 @@ Lemma merge_unfold n m : merge n m = | 0 => 0 | S n' => merge n' m end. -Proof. intros. unfold_sub merge (merge n m). simpl. destruct n ; reflexivity. Qed. +Proof. intros. unfold merge at 1. unfold merge_func. + unfold_sub merge (merge n m). + simpl. destruct n ; reflexivity. +Qed. Print merge. |