From a393a49c9c24210faa656d5355e3b213aca2e8ba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 1 Aug 2016 15:13:21 -0700 Subject: Better hint for div_to_inv_modulo It needs to infer x' --- src/Util/ZUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util') 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. -- cgit v1.2.3