diff options
| author | Emilio Jesus Gallego Arias | 2018-09-27 01:44:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-27 01:44:01 +0200 |
| commit | a324989b7dea4a1db59fc7c373bd3fa5cb60f09a (patch) | |
| tree | 5aa0f789a9ddbefc267cb41ac774d9217e6086be /theories | |
| parent | 71296e6e91de5b3fea08ef4b34426a02304f00b8 (diff) | |
[stdlib] Fix warning due to missing Declare Scope in Bvector
This broke the build so it should be merged quickly.
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Bool/Bvector.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 4eb05d12f1..3d615485b9 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -102,6 +102,7 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := End BOOLEAN_VECTORS. Module BvectorNotations. +Declare Scope Bvector_scope. Delimit Scope Bvector_scope with Bvector. Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope. Infix "^&" := (BVand _) (at level 40, left associativity) : Bvector_scope. |