diff options
| author | Brian Campbell | 2019-05-23 18:21:00 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-05-23 18:21:34 +0100 |
| commit | bb5b6a4389ab0b289ad3366322a487c18b6ba763 (patch) | |
| tree | 93f18c62a3cd1090714a7d10aadef737b1bee9c0 /lib/coq | |
| parent | 5bbfc39ff20f208704453249f02d468325917055 (diff) | |
Coq: solve some division constraints
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_values.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index ab7ed07e..04fc3413 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1360,7 +1360,14 @@ tauto. Qed. Ltac solve_euclid := -repeat match goal with |- context [ZEuclid.modulo ?x ?y] => +repeat match goal with +| |- context [ZEuclid.modulo ?x ?y] => + specialize (ZEuclid.div_mod x y); + specialize (ZEuclid.mod_always_pos x y); + generalize (ZEuclid.modulo x y); + generalize (ZEuclid.div x y); + intros +| |- context [ZEuclid.div ?x ?y] => specialize (ZEuclid.div_mod x y); specialize (ZEuclid.mod_always_pos x y); generalize (ZEuclid.modulo x y); |