From 59adf48b33e49ea07ee1ab0984be066f60115041 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 19 Apr 2019 14:42:14 +0100
Subject: Coq: more robust handling of unknown constraints

---
 lib/coq/Sail2_values.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 67b76416..8c9c40a3 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1225,9 +1225,10 @@ Ltac prepare_for_solver :=
  unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
  reduce_pow;
- (* omega doesn't cope well with extra "True"s in the goal *)
- repeat setoid_rewrite True_left;
- repeat setoid_rewrite True_right.
+ (* omega doesn't cope well with extra "True"s in the goal.
+    Check that they actually appear because setoid_rewrite can fill in evars. *)
+ repeat match goal with |- context[True /\ _] => setoid_rewrite True_left end;
+ repeat match goal with |- context[_ /\ True] => setoid_rewrite True_right end.
 
 Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x).
 constructor.
@@ -1292,7 +1293,7 @@ prepare_for_solver;
 constructor;
 repeat match goal with |- and _ _ => split end;
  solve
- [ match goal with |- (?x _) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) _) end
+ [ match goal with |- (?x ?y) => is_evar x; idtac "Warning: unknown constraint"; exact (I : (fun _ => True) y) end
  | apply ArithFact_mword; assumption
  | omega with Z
    (* Try sail hints before dropping the existential *)
-- 
cgit v1.2.3