From 2e67ff1b33d05b9efc020de664f3200f9ff0d479 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 21 Feb 2008 13:54:00 +0000
Subject: congruence now knows about _ -> _

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

(limited to 'test-suite')

diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index fecc897722..94d827fd5c 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -78,6 +78,14 @@ intros.
  congruence.
 Qed.
 
+(* example with implications *)
+
+Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D  -> 
+(A -> C) = (B -> D).
+congruence.
+Qed.
+
+
 Set Implicit Arguments.
 
 Parameter elt: Set.
@@ -94,5 +102,6 @@ Proof.
   auto.
 Qed.
             
+
             
             
\ No newline at end of file
-- 
cgit v1.2.3