From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- test-suite/success/apply.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'test-suite/success/apply.v') 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. -- cgit v1.2.3