Coq: tweak disjunctions tactic with subst to support more constraints

1 files changed, 2 insertions, 1 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 61e2c6a4..ab7ed07e 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1447,7 +1447,8 @@ Ltac main_solver :=
  | match goal with |- context [Z.mul] => nia end
  (* If we have a disjunction from a set constraint on a variable we can often
     solve a goal by trying them (admittedly this is quite heavy handed...) *)
- | let aux x :=
+ | subst;
+   let aux x :=
     is_var x;
     intuition (subst;auto)
    in