diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-03-20 17:09:44 -0400 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-03-20 17:09:44 -0400 |
| commit | dc51191d484348bf827f91fd4ee5dd088fd5e17b (patch) | |
| tree | efcec532cdb798e77841bd9503493109ff9892c6 /src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | |
| parent | 2f178e16ab2e44b6139ef01dca17f425f02bb319 (diff) | |
made BaseVector instance global
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParamProofs.v')
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 847b8e85f..93e6bc1f0 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -268,7 +268,7 @@ Section PseudoMersenneBaseParamProofs. rewrite <- base_length; assumption. Qed. - Instance bv : BaseSystem.BaseVector base := { + Global Instance bv : BaseSystem.BaseVector base := { base_positive := base_positive; b0_1 := b0_1; base_good := base_good |