From 4cfc0a4e8037fde12a18434cd6c229db14d4b9e5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 12 Nov 2017 00:42:11 -0500 Subject: Use abstract in ring autosolve --- src/Util/SideConditions/RingPackage.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/RingPackage.v b/src/Util/SideConditions/RingPackage.v index ef01dd069..3cb7b64da 100644 --- a/src/Util/SideConditions/RingPackage.v +++ b/src/Util/SideConditions/RingPackage.v @@ -31,6 +31,6 @@ Ltac Zring_prod_eq_tac _ := Ltac autosolve else_tac := lazymatch goal with | [ |- eq_by_Zring_prod_package _ ] - => solve [ Zring_prod_eq_tac () ] + => abstract Zring_prod_eq_tac () | _ => else_tac () end. -- cgit v1.2.3