diff --git a/processor/src/processor/KamiRiscvStep.v b/processor/src/processor/KamiRiscvStep.v
index a210d6078..5c8d685bc 100644
--- a/processor/src/processor/KamiRiscvStep.v
+++ b/processor/src/processor/KamiRiscvStep.v
@@ -1704,7 +1704,7 @@ Section Equiv.
       all: simpl_bit_manip.
 
       (** Evaluation of riscv-coq decode/execute *)
-      
+
       all: eval_decode.
       all: try subst opcode; try subst funct3; try subst funct6; try subst funct7;
         try subst shamtHi; try subst shamtHiTest.
@@ -1721,7 +1721,7 @@ Section Equiv.
                | H : Z |- _ => clear H
                | H : list Instruction |- _ => clear H
                | H : Instruction |- _ => clear H
-          end.
+               end.
 
       all: set (v' := if Z.eq_dec rs1 0 then word.of_Z 0
                       else match map.get rrf rs1 with
@@ -1744,7 +1744,7 @@ Section Equiv.
       all: try match goal with
                | [H: match Memory.load_bytes ?sz ?m ?a with | Some _ => _ | None => _ end |- _] =>
                  destruct (Memory.load_bytes sz m a) as [lv|] eqn:Hlv; [exfalso|]
-             end.
+               end.
       all: subst v; rewrite Hv' in *. 
       all: try (subst v' oimm12;
                 regs_get_red Hlv;
@@ -1898,7 +1898,7 @@ Section Equiv.
                | H : Z |- _ => clear H
                | H : list Instruction |- _ => clear H
                | H : Instruction |- _ => clear H
-          end.
+               end.
 
       all: set (v' := if Z.eq_dec rs1 0 then word.of_Z 0
                       else match map.get rrf rs1 with
@@ -2166,7 +2166,7 @@ Section Equiv.
                | H : Z |- _ => clear H
                | H : list Instruction |- _ => clear H
                | H : Instruction |- _ => clear H
-          end.
+               end.
 
       all: set (v' := if Z.eq_dec rs1 0 then word.of_Z 0
                       else match map.get rrf rs1 with
@@ -2657,7 +2657,7 @@ Section Equiv.
                | H : Z |- _ => clear H
                | H : list Instruction |- _ => clear H
                | H : Instruction |- _ => clear H
-          end.
+               end.
 
       all: set (v' := if Z.eq_dec rs1 0 then word.of_Z 0
                       else match map.get rrf rs1 with