From 294ff935decaf8450bf3d3557218b936b473ce0b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 23 Jul 2018 16:15:29 +0100
Subject: Coq: faster MIPS extras without confusing message

---
 mips/mips_extras.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index cc905f11..6a6aed5c 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -140,7 +140,7 @@ Definition eq_bit (x : bitU) (y : bitU) : bool :=
 
 Require Import Zeuclid.
 Definition euclid_modulo (m n : Z) `{ArithFact (n > 0)} : {z : Z & ArithFact (0 <= z <= n-1)}.
-refine (build_ex (ZEuclid.modulo m n)).
+refine (existT _ (ZEuclid.modulo m n) _).
 constructor.
 destruct H.
 assert (Zabs n = n). { rewrite Zabs_eq; auto with zarith. }
-- 
cgit v1.2.3