From dc51191d484348bf827f91fd4ee5dd088fd5e17b Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Sun, 20 Mar 2016 17:09:44 -0400 Subject: made BaseVector instance global --- src/BaseSystem.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/BaseSystem.v') 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]. *) -- cgit v1.2.3