diff options
Diffstat (limited to 'test-suite/success/apply.v')
| -rw-r--r-- | test-suite/success/apply.v | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index e3183ef2..d3c76101 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -97,13 +97,14 @@ Qed. (* Check use of unification of bindings types in specialize *) +Module Type Test. Variable P : nat -> Prop. Variable L : forall (l : nat), P l -> P l. Goal P 0 -> True. intros. specialize L with (1:=H). Abort. -Reset P. +End Test. (* Two examples that show that hnf_constr is used when unifying types of bindings (a simplification of a script from Field_Theory) *) @@ -415,3 +416,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. |