From 00c579e603478d452959dde0ec61672d7b5d27a4 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 17 Jun 2020 23:08:32 +0100
Subject: Some (very) useful lemmas about arrays.

---
 src/common/Coquplib.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/common')

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 675ad23..efa1323 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -52,6 +52,8 @@ Ltac clear_obvious :=
 
 Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate.
 
+Global Opaque Nat.div.
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
-- 
cgit