aboutsummaryrefslogtreecommitdiff
path: root/src/BaseSystem.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/BaseSystem.v')
-rw-r--r--src/BaseSystem.v2
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 ->