From a76ad2ccdc57f54bd23e1c64f3f4a4af8e912050 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 16 Mar 2008 13:40:45 +0000 Subject: Reorganize Program and Classes theories. Requiring Setoid no longer sets implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Relation_Operators.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 61b70ba68..a5ad269d4 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. Inductive le_AsB : A + B -> A + B -> Prop := - | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y) - | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y) - | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y). + | le_aa : forall x y:A, leA x y -> le_AsB (inl _ x) (inl _ y) + | le_ab : forall (x:A) (y:B), le_AsB (inl _ x) (inr _ y) + | le_bb : forall x y:B, leB x y -> le_AsB (inr _ x) (inr _ y). End Disjoint_Union. -- cgit v1.2.3