From 991dd7696058770d384b2aee3be0097f9af8d35d Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 9 Aug 2018 11:16:41 +0100
Subject: Coq: a bit more handling of unknown constraints

---
 lib/coq/Sail2_values.v | 20 ++++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index e4fff741..14ed0459 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1017,12 +1017,20 @@ Ltac prepare_for_solver :=
 Ltac solve_arithfact :=
 prepare_for_solver;
 (*dump_context;*)
- solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; instantiate (1 := fun _ => True); constructor; constructor end
-       | apply ArithFact_mword; assumption
-       | constructor; omega with Z
-         (* The datatypes hints give us some list handling, esp In *)
-       | constructor; eauto 3 with datatypes zarith sail
-       | constructor; idtac "Unable to solve constraint"; dump_context; fail].
+ solve
+ [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end
+ | match goal with |- ArithFact (?x = ?y) =>
+   (is_evar x || is_evar y);
+   (* compute to allow projections to remove proofs that might not be allowed in the evar *)
+   let x := eval cbn in x in
+   let y := eval cbn in y in
+   idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end
+ | apply ArithFact_mword; assumption
+ | constructor; omega with Z
+   (* The datatypes hints give us some list handling, esp In *)
+ | constructor; eauto 3 with datatypes zarith sail
+ | constructor; idtac "Unable to solve constraint"; dump_context; fail
+ ].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
 
 Hint Unfold length_mword : sail.
-- 
cgit v1.2.3