diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-01 15:13:21 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-01 15:13:21 -0700 |
| commit | a393a49c9c24210faa656d5355e3b213aca2e8ba (patch) | |
| tree | 229069c717fa4aaa89f20f552f125a590c17763c /src | |
| parent | c462b6e63b2fd829f3013a38446fcf5f6ee7bcd7 (diff) | |
Better hint for div_to_inv_modulo
It needs to infer x'
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index b7d460fb3..45e53277f 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1258,7 +1258,7 @@ Module Z. reflexivity. Qed. End equiv_modulo. - Hint Rewrite div_to_inv_modulo using lia : zstrip_div. + Hint Rewrite div_to_inv_modulo using solve [ eassumption | lia ] : zstrip_div. Module EquivModuloInstances (dummy : Nop). (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=4973 *) Existing Instance equiv_modulo_Reflexive. |