From 7e6ce51bf1a7beea6fa7818d2e5447ade79c30e7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Apr 2008 21:39:08 +0000
Subject: Quelques bricoles autour de l'unification: - Un patch pour le bug de
 non vérification du typage de Stéphane L. - Changement du fameux message
 "cannot solve a second-order matching problem"   en espérant, à défaut de
 savoir résoudre plus souvent le problème, que   le message est plus
 explicite. - Divers changements cosmétiques.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10860 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/apply.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 3b4e8af21f..e3fed09e7d 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -174,3 +174,15 @@ Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y.
 Theorem t : r true false.
 apply ax with (R := r).
 Qed.
+
+
+(* Check verification of type at unification (Submitted by Stéphane Lengrand)
+   (without verification, the first "apply" works which leads to wrongly
+   instantiate x by Prop) *)
+
+Theorem t: ~(forall x:Prop, ~x).
+unfold not.
+intro.
+eapply H.
+apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I).
+Defined.
-- 
cgit v1.2.3