From 7ce8915a2f29b45a6be029c89b671f80cc3b7634 Mon Sep 17 00:00:00 2001 From: pboutill Date: Tue, 26 Jul 2011 11:30:29 +0000 Subject: All the parameters of Compare are implicits. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14297 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/OrderedType.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 9efb68ab3..5d8773957 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -20,6 +20,10 @@ Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := | EQ : eq x y -> Compare lt eq x y | GT : lt y x -> Compare lt eq x y. +Implicit Arguments LT [X lt eq x y]. +Implicit Arguments EQ [X lt eq x y]. +Implicit Arguments GT [X lt eq x y]. + Module Type MiniOrderedType. Parameter Inline t : Type. @@ -141,7 +145,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_eq : forall x y : t, - eq x y -> exists H : eq x y, compare x y = EQ _ H. + eq x y -> exists H : eq x y, compare x y = EQ H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -149,7 +153,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_lt : forall x y : t, - lt x y -> exists H : lt x y, compare x y = LT _ H. + lt x y -> exists H : lt x y, compare x y = LT H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. @@ -157,7 +161,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma elim_compare_gt : forall x y : t, - lt y x -> exists H : lt y x, compare x y = GT _ H. + lt y x -> exists H : lt y x, compare x y = GT H. Proof. intros; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. -- cgit v1.2.3