diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-17 15:57:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-17 15:57:43 +0000 |
| commit | 991ea521f4e34afa45f33906091c34116d2c0f63 (patch) | |
| tree | ddb5ba679e3777a894736699d9277142d54da8d5 | |
| parent | 211030a7a870bdf3bc36b0923379e2d1bf6c729a (diff) | |
Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.eq_dec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11694 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. |