diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 47fa2fda..b29963b6 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1802,8 +1802,21 @@ Ltac run_main_solver := | run_main_solver_impl (* for cases where there's an evar in the goal *) ]. +Ltac is_fixpoint ty := + match ty with + | forall _reclimit, Acc _ _reclimit -> _ => idtac + | _ -> ?res => is_fixpoint res + end. + +Ltac clear_fixpoints := + repeat + match goal with + | H:_ -> ?res |- _ => is_fixpoint res; clear H + end. + Ltac solve_arithfact := intros; (* To solve implications for derive_m *) + clear_fixpoints; (* Avoid using recursive calls *) solve [ solve_unknown | match goal with |- ArithFact (?x <= ?x <= ?x) => exact trivial_range end |