diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/apply.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 454a118d61..3c9fbeb364 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -20,3 +20,11 @@ intros. apply n_Sn in H. assumption. Qed. + +(* Check naming in with bindings; printing used to be inconsistent before *) +(* revision 9450 *) + +Notation S':=S (only parsing). +Goal (forall S, S = S' S) -> (forall S, S = S' S). +intros. +apply H with (S0 := S). |