From 29c881414cf1ae7c6c882c1285f72b5d5cba1b4e Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 15 Dec 2020 20:51:29 -0800
Subject: Modify Classes/DecidableClass.v to compile with -mangle-names

---
 theories/Classes/DecidableClass.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 7169aa673d..cd6765bab9 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -46,7 +46,7 @@ Qed.
 (** The generic function that should be used to program, together with some
   useful tactics. *)
 
-Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
+Definition decide P {H : Decidable P} := @Decidable_witness _ H.
 
 Ltac _decide_ P H :=
   let b := fresh "b" in
-- 
cgit v1.2.3