diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 3 |
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 |