From cd6c4f1297a6604fa4691a5f13808b721194f13b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 2 Jul 2016 12:08:02 -0700 Subject: Make ZUtil more uniform The standard library uses Z.*, and Z* and Z_* are compatibility notations. We follow suit. Also, eliminate a few lemmas that are duplicates of ones in the standard library. --- src/BaseSystemProofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/BaseSystemProofs.v') diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 85835aabe..5746cb5f1 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -177,7 +177,7 @@ Section BaseSystemProofs. Lemma nth_error_base_nonzero : forall n x, nth_error base n = Some x -> x <> 0. Proof. - eauto using (@nth_error_value_In Z), Zgt0_neq0, base_positive. + eauto using (@nth_error_value_In Z), Z.gt0_neq0, base_positive. Qed. Hint Rewrite plus_0_r. -- cgit v1.2.3