diff options
| author | Brian Campbell | 2018-08-02 16:35:47 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-02 18:16:55 +0100 |
| commit | 03dcb84bb8330cfa7b947ff4ecc0c5c9efca8ab0 (patch) | |
| tree | 35aba0897f410cab13e52a1f9c0e304f12c4290a | |
| parent | 8a06df3ad1b90a355d3e5adb694002f00e67823e (diff) | |
Coq: limit eauto to ensure termination in reasonable time
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |