From 612ea3d4b3c7d7e00616b009050803cd7b7f763e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Jan 2007 17:36:04 +0000
Subject: Correction d'un bug d'unification-pattern dans l'algo d'unification
 des tactiques (ne marchait que si l'instance était une application).

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

(limited to 'test-suite')

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 7acbb7d05e..2d6dabf264 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -15,6 +15,12 @@ Proof.
 intros; apply (H _ H0).
 Qed.
 
+Lemma l3 : (forall P, ~(exists x:nat, P x))
+         -> forall P:nat->Prop, ~(exists x:nat, P x -> P x).
+Proof.
+intros; apply H.
+Qed.
+
 
 (* Example submitted for Zenon *)
 
-- 
cgit v1.2.3