From bb5b6a4389ab0b289ad3366322a487c18b6ba763 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 23 May 2019 18:21:00 +0100
Subject: Coq: solve some division constraints

---
 lib/coq/Sail2_values.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index ab7ed07e..04fc3413 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1360,7 +1360,14 @@ tauto.
 Qed.
 
 Ltac solve_euclid :=
-repeat match goal with |- context [ZEuclid.modulo ?x ?y] =>
+repeat match goal with
+| |- context [ZEuclid.modulo ?x ?y] =>
+  specialize (ZEuclid.div_mod x y);
+  specialize (ZEuclid.mod_always_pos x y);
+  generalize (ZEuclid.modulo x y);
+  generalize (ZEuclid.div x y);
+  intros
+| |- context [ZEuclid.div ?x ?y] =>
   specialize (ZEuclid.div_mod x y);
   specialize (ZEuclid.mod_always_pos x y);
   generalize (ZEuclid.modulo x y);
-- 
cgit v1.2.3