diff options
| -rw-r--r-- | theories/FSets/OrderedType.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v index 8a2f0502a..8c4c6818a 100644 --- a/theories/FSets/OrderedType.v +++ b/theories/FSets/OrderedType.v @@ -311,6 +311,9 @@ Ltac false_order := elimtype False; order. Ltac elim_comp_gt x y := elim (elim_compare_gt (x:=x) (y:=y)); [ intros _1 _2; rewrite _2; clear _1 _2 | auto ]. + + (** For compatibility reasons *) + Definition eq_dec := eq_dec. Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. |