diff options
| author | Brian Campbell | 2018-12-20 16:41:39 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-12-27 15:38:30 +0000 |
| commit | cb5773b3b4d69750f9693e9c9f4e20de5e06ed3b (patch) | |
| tree | a4ce3bfbc8dba945d84129bef08ae8efae85c626 | |
| parent | f70f187dbf667df5e8610978e928d9ba76af8e0e (diff) | |
Coq: make solver try hints before stripping away existentials
(which allows us to avoid a Coq bug where the proof isn't recorded
correctly)
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index b7e9bbc9..e3e039c2 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1180,6 +1180,8 @@ prepare_for_solver; [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end | apply ArithFact_mword; assumption | constructor; omega with Z + (* Try sail hints before dropping the existential *) + | constructor; eauto 3 with zarith sail (* The datatypes hints give us some list handling, esp In *) | constructor; drop_exists; eauto 3 with datatypes zarith sail | constructor; idtac "Unable to solve constraint"; dump_context; fail |