diff options
| author | Jasper Hugunin | 2020-08-25 13:10:40 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | c16e4c23e6591aace243c5503ce70e99d3c0569d (patch) | |
| tree | 4745badc6f33ae6ae81aaf27c91e3efc18287c24 | |
| parent | 32240c45be0835b6b32eec6f85743fa3c4c15537 (diff) | |
Modify Structures/GenericMinMax.v to compile with -mangle-names
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v index 8d20ce77f9..1af6aebec6 100644 --- a/theories/Structures/GenericMinMax.v +++ b/theories/Structures/GenericMinMax.v @@ -629,9 +629,9 @@ Module TOMaxEqDec_to_Compare if eq_dec x y then Eq else if eq_dec (M.max x y) y then Lt else Gt. - Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). + Lemma compare_spec x y : CompSpec eq lt x y (compare x y). Proof. - intros; unfold compare; repeat destruct eq_dec; auto; constructor. + unfold compare; repeat destruct eq_dec; auto; constructor. - destruct (lt_total x y); auto. absurd (x==y); auto. transitivity (max x y); auto. symmetry. apply max_l. rewrite le_lteq; intuition. |