diff options
| author | Jasper Hugunin | 2020-08-25 13:05:49 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | 17ed93c2caadfcf3a2aee8f2b9683191063b2951 (patch) | |
| tree | fc8955ee8594e1de7b8a9edc4e699291c1e5c10c | |
| parent | e5880b643bb9ce6974d3ecffd8edcbfad9f45cd4 (diff) | |
Modify Structures/Orders.v to compile with -mangle-names
| -rw-r--r-- | theories/Structures/Orders.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 94938c1d4d..b3e3b6e853 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -165,7 +165,7 @@ End OT_to_Full. Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O. Lemma lt_total : forall x y, x<y \/ x==y \/ y<x. - Proof. intros; destruct (compare_spec x y); auto. Qed. + Proof. intros x y; destruct (compare_spec x y); auto. Qed. End OTF_LtIsTotal. Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder @@ -250,7 +250,7 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Lemma leb_le : forall x y, leb x y <-> x <= y. Proof. - intros. unfold leb. rewrite le_lteq. + intros x y. unfold leb. rewrite le_lteq. destruct (compare_spec x y) as [EQ|LT|GT]; split; auto. - discriminate. - intros LE. elim (StrictOrder_Irreflexive x). @@ -261,7 +261,7 @@ Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool. Lemma leb_total : forall x y, leb x y \/ leb y x. Proof. - intros. rewrite 2 leb_le. rewrite 2 le_lteq. + intros x y. rewrite 2 leb_le. rewrite 2 le_lteq. destruct (compare_spec x y); intuition. Qed. @@ -302,7 +302,7 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. - intros. unfold compare. + intros x y. unfold compare. case_eq (x <=? y). - case_eq (y <=? x). + constructor. split; auto. @@ -352,7 +352,7 @@ Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull. Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y. Proof. - intros. + intros x y. unfold lt, eq, le. split; [ | intuition ]. intros LE. |