diff options
| author | Brian Campbell | 2018-08-03 15:04:18 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-03 15:04:18 +0100 |
| commit | baabef2bc2d39fc47ba47cd2ac5305856dd212a2 (patch) | |
| tree | e4d90f0eb109b0cf4e1eff6d21073720ea9f29b4 /lib | |
| parent | 2cb15665392d0b87da9e0c1f43e19267f28c3a82 (diff) | |
Coq: use a dummy constraint when the real one is unknown
Not really what we want, but a useful placeholder because of the
widespread use of ex_int.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index acd11b45..e4fff741 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1017,7 +1017,8 @@ Ltac prepare_for_solver := Ltac solve_arithfact := prepare_for_solver; (*dump_context;*) - solve [apply ArithFact_mword; assumption + solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; instantiate (1 := fun _ => True); constructor; constructor end + | apply ArithFact_mword; assumption | constructor; omega with Z (* The datatypes hints give us some list handling, esp In *) | constructor; eauto 3 with datatypes zarith sail |