From baabef2bc2d39fc47ba47cd2ac5305856dd212a2 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 3 Aug 2018 15:04:18 +0100
Subject: Coq: use a dummy constraint when the real one is unknown Not really
 what we want, but a useful placeholder because of the widespread use of
 ex_int.

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

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index acd11b45..e4fff741 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1017,7 +1017,8 @@ Ltac prepare_for_solver :=
 Ltac solve_arithfact :=
 prepare_for_solver;
 (*dump_context;*)
- solve [apply ArithFact_mword; assumption
+ 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
-- 
cgit v1.2.3