Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

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.