diff --git a/README.md b/README.md
index bce8cdf..18212af 100644
--- a/README.md
+++ b/README.md
@@ -131,23 +131,23 @@ syntax approaching math-mode signatures. We illustrate both below.
 
 - The signature DSL is defined by the following BNF:
 
-      baseprop  ::=  modname -<-> modname       (monotonicity)
-                  |  modname -$-> modname       (strictness)
-                  |  modname -~-> modname       (invariance)
+        baseprop  ::=  modname -<-> modname       (monotonicity)
+                    |  modname -$-> modname       (strictness)
+                    |  modname -~-> modname       (invariance)
 
-          prop  ::=  '(testsig' (modname '--->')* baseprop ('--->' modname)*) ')' 'for_op'
+            prop  ::=  '(testsig' (modname '--->')* baseprop ('--->' modname)*) ')' 'for_op'
 
 
   For example,
 
-      (testsig (module L) -<-> (module L)) for_op
+        (testsig (module L) -<-> (module L)) for_op
 
   specifies monotonicity of a function from L to L.
 
 
   For a more advanced example,
 
-      (testsig (module L) ---> (module L) -<-> (module L) ---> (module L) ---> (module L)) for_op
+        (testsig (module L) ---> (module L) -<-> (module L) ---> (module L) ---> (module L)) for_op
 
   specifies monotonicity in the second argument of a function with
   signature L -> L -> L -> L -> L.
@@ -164,43 +164,43 @@ syntax approaching math-mode signatures. We illustrate both below.
 
 - The combinator DSL is defined by the following BNF:
 
-      modname   ::=  '(module' NAME ')'
-    
-      baseprop  ::=  op_monotone
-                  |  op_strict
-                  |  op_invariant
-    
-      rightprop ::=  baseprop
-                  |  pw_right modname '(' rightprop ')'
-    
-      leftprop  ::=  rightprop
-                  |  pw_left modname '(' leftprop ')'
-    
-      prop      ::=  'finalize (' leftprop modname modname ')'
+        modname   ::=  '(module' NAME ')'
+      
+        baseprop  ::=  op_monotone
+                    |  op_strict
+                    |  op_invariant
+      
+        rightprop ::=  baseprop
+                    |  pw_right modname '(' rightprop ')'
+      
+        leftprop  ::=  rightprop
+                    |  pw_left modname '(' leftprop ')'
+      
+        prop      ::=  'finalize (' leftprop modname modname ')'
 
 
   Argument modules to pw_left and pw_right has to match the following
   signature (an element type, a generator, and a string coercion
   function):
 
-      module type ARB_ARG =
-      sig
-        type elem
-        val arb_elem    : elem Arbitrary.t
-        val to_string   : elem -> string
-      end
+        module type ARB_ARG =
+        sig
+          type elem
+          val arb_elem    : elem Arbitrary.t
+          val to_string   : elem -> string
+        end
 
 
   Revising the example above,
 
-    finalize (op_monotone (module L) (module L))
+        finalize (op_monotone (module L) (module L))
 
   specifies monotonicity of a function from L to L.
 
 
   Revising the more advanced example above,
 
-    finalize (pw_left (module L) (pw_right (module L) (pw_right (module L) op_monotone)) (module L) (module L))
+        finalize (pw_left (module L) (pw_right (module L) (pw_right (module L) op_monotone)) (module L) (module L))
 
   specifies monotonicity in the second argument of a function with
   signature L -> L -> L -> L -> L.