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/BaseSystem.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/BaseSystem.v') diff --git a/src/BaseSystem.v b/src/BaseSystem.v index 743cdfde8..c22af95ca 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -111,7 +111,7 @@ Section PolynomialBaseCoefs. rewrite in_map_iff in *. destruct H; destruct H. subst. - apply pos_pow_nat_pos. + apply Z.pos_pow_nat_pos. Qed. Lemma poly_base_defn : forall i, (i < length poly_base)%nat -> -- cgit v1.2.3