From c16e4c23e6591aace243c5503ce70e99d3c0569d Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 25 Aug 2020 13:10:40 -0700
Subject: Modify Structures/GenericMinMax.v to compile with -mangle-names

---
 theories/Structures/GenericMinMax.v | 4 ++--
 1 file 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.
-- 
cgit v1.2.3