diff options
Diffstat (limited to 'theories/Structures/OrderedType2Ex.v')
| -rw-r--r-- | theories/Structures/OrderedType2Ex.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v index 801c18723b..6a02319734 100644 --- a/theories/Structures/OrderedType2Ex.v +++ b/theories/Structures/OrderedType2Ex.v @@ -77,7 +77,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. | Gt => Gt end. - Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). + Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. intros (x1,x2) (y1,y2); unfold compare; simpl. destruct (O1.compare_spec x1 y1); try (constructor; compute; auto). |