aboutsummaryrefslogtreecommitdiff
path: root/src/BaseSystem.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/BaseSystem.v')
-rw-r--r--src/BaseSystem.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index f3a1a0fdb..627550440 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -85,6 +85,7 @@ Section BaseSystem.
End BaseSystem.
+(* Example : polynomial base system *)
Section PolynomialBaseCoefs.
Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true).
(** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *)