diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-26 11:30:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-26 11:30:29 +0000 |
| commit | 7ce8915a2f29b45a6be029c89b671f80cc3b7634 (patch) | |
| tree | 8ff9c8388f3390b771f2402f78e10b7a733d0095 /theories/Structures | |
| parent | dc6d09002e9de32434f558565905dc74af8ad62c (diff) | |
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
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrderedType.v | 10 |
1 files changed, 7 insertions, 3 deletions
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. |