From cceb7c96062ade251deb604bb21737ab0d15eae4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 3 Sep 2018 18:51:18 +0100
Subject: Coq: solver should split earlier otherwise some other parts don't
 work properly. Also update RISC-V patch.

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 6b75bd47..7a9d16be 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1039,14 +1039,14 @@ Ltac prepare_for_solver :=
  clear_irrelevant_defns;
  clear_non_Z_defns;
  autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *)
+ split_cases;
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
  unfold_In;
  unbool_comparisons;
  reduce_list_lengths;
- reduce_pow;
- split_cases.
+ reduce_pow.
 
 Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x).
 constructor.
-- 
cgit v1.2.3