From 2a0308893fdca3063dc5888586e03fdc03afa86c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Aug 2007 09:07:19 +0000 Subject: [PATCH] alpha conversion to avoid case-insensitivity of MySql on my laptop. OK, I know, I should fix it... --- matita/tests/coercions_contravariant.ma | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/matita/tests/coercions_contravariant.ma b/matita/tests/coercions_contravariant.ma index b1656aeca..64f85ea75 100644 --- a/matita/tests/coercions_contravariant.ma +++ b/matita/tests/coercions_contravariant.ma @@ -21,10 +21,10 @@ axiom A : nat -> Type. axiom B : nat -> Type. axiom A1: nat -> Type. axiom B1: nat -> Type. -axiom b : ∀n.B n. axiom c : ∀n,m. A1 n -> A m. axiom d : ∀n,m. B n -> B1 m. axiom f : ∀n,m. A n -> B m. +axiom g : ∀n.B n. coercion cic:/matita/test/c.con. coercion cic:/matita/test/d.con. @@ -32,8 +32,7 @@ coercion cic:/matita/test/d.con. definition foo := λn,n1,m,m1.(λx.d m m1 (f n m (c n1 n x)) : A1 n1 -> B1 m1). definition foo1_1 := λn,n1,m,m1.(f n m : A1 n1 -> B1 m1). -definition g := λn,m.λx:A n.b m. -definition foo2 := λn,n1,m,m1.(g n m : A1 n1 -> B1 m1). -definition foo3 := λn1,n,m,m1.(g n m : A1 n1 -> B1 m1). -definition foo4 := λn1,n,m1,m.(g n m : A1 n1 -> B1 m1). - +definition h := λn,m.λx:A n.g m. +definition foo2 := λn,n1,m,m1.(h n m : A1 n1 -> B1 m1). +definition foo3 := λn1,n,m,m1.(h n m : A1 n1 -> B1 m1). +definition foo4 := λn1,n,m1,m.(h n m : A1 n1 -> B1 m1). \ No newline at end of file -- 2.39.2