From 1bd3a2601bc0b5637f650810ff8a9e108e79d043 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 25 Oct 2019 17:46:33 +0100
Subject: Coq: make sure solver can't accidentally use recursive definitions

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

(limited to 'lib')

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
-- 
cgit v1.2.3