diff options
author | Jason Gross <jagro@google.com> | 2016-07-02 12:08:02 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-02 12:18:52 -0700 |
commit | cd6c4f1297a6604fa4691a5f13808b721194f13b (patch) | |
tree | 71075b2573818cae036f87a7efda7f3372eb4e3e /src/BaseSystem.v | |
parent | 2939418894d78c095cd9142ce99c615f2d61dda6 (diff) |
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.
Diffstat (limited to 'src/BaseSystem.v')
-rw-r--r-- | src/BaseSystem.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |