From 03dcb84bb8330cfa7b947ff4ecc0c5c9efca8ab0 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Aug 2018 16:35:47 +0100
Subject: Coq: limit eauto to ensure termination in reasonable time

---
 lib/coq/Sail2_values.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 6fcbbb52..41414c96 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1020,7 +1020,7 @@ prepare_for_solver;
  solve [apply ArithFact_mword; assumption
        | constructor; omega with Z
          (* The datatypes hints give us some list handling, esp In *)
-       | constructor; eauto with datatypes zarith sail
+       | constructor; eauto 3 with datatypes zarith sail
        | constructor; idtac "Unable to solve constraint"; dump_context; fail].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
 
-- 
cgit v1.2.3