From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- theories/Numbers/Natural/BigN/NMake.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Numbers/Natural/BigN/NMake.v') diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 98949736..1425041a 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType. Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. -- cgit v1.2.3