From 2d01a4794e4a684d9868ab7e7e58966a12161de7 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 25 Aug 2020 13:07:08 -0700
Subject: Modify Structures/OrdersTac.v to compile with -mangle-names

---
 theories/Structures/OrdersTac.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 408348139d..1c8073972d 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -100,9 +100,9 @@ Definition interp_ord o :=
  match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
 Local Notation "#" := interp_ord.
 
-Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
+Lemma trans o o' x y z : #o x y -> #o' y z -> #(o+o') x z.
 Proof.
-destruct o, o'; simpl; intros x y z;
+destruct o, o'; simpl;
 rewrite ?P.le_lteq; intuition auto;
 subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.
-- 
cgit v1.2.3