Added ability to take the type of applied metas into account when

instantiating them in the unification algorithm used for tactics.
This allows to discard ill-typed uses of first-order unification which
otherwise would have been fatal (this incidentally allows to partially
restore some compatibility with 8.3 that was broken after eta was
added in unification).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 32d82bd1a8..e3183ef279 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -397,3 +397,21 @@ intro x;
 apply x.
 
 *)
+
+Section A.
+
+Variable map : forall (T1 T2 : Type) (f : T1 -> T2) (t11 t12 : T1),
+  identity (f t11) (f t12).
+
+Variable mapfuncomp : forall (X Y Z : Type) (f : X -> Y) (g : Y -> Z) (x x' : X),
+  identity (map Y Z g (f x) (f x')) (map X Z (fun x0 : X => g (f x0)) x x').
+
+Goal forall X:Type, forall Y:Type, forall f:X->Y, forall x : X, forall x' : X, 
+  forall g : Y -> X,
+  let gf := (fun x : X => g (f x)) : X -> X in
+   identity (map Y X g (f x) (f x')) (map X X gf x x').
+intros.
+apply mapfuncomp.
+Abort.
+
+End A.