Extend the frontend language with break/continue, named variables, and static

variables.

theories/base.v

@@ -407,15 +407,18 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
 Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
-Notation "'( x1 , x2 ) ← y ; z" :=
+Notation "' ( x1 , x2 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1, x2) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Notation "'( x1 , x2 , x3 ) ← y ; z" :=
+Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Notation "'( x1 , x2 , x3  , x4 ) ← y ; z" :=
+Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
+  (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
+  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.