diff options
Diffstat (limited to 'test-suite/success/apply.v')
| -rw-r--r-- | test-suite/success/apply.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index e3183ef27..8e829e061 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -415,3 +415,17 @@ apply mapfuncomp. Abort. End A. + +(* Check "with" clauses refer to names as they are printed *) + +Definition hide p := forall n:nat, p = n. + +Goal forall n, (forall n, n=0) -> hide n -> n=0. +unfold hide. +intros n H H'. +(* H is displayed as (forall n, n=0) *) +apply H with (n:=n). +Undo. +(* H' is displayed as (forall n0, n=n0) *) +apply H' with (n0:=0). +Qed. |