m

mit-plv · Jan 10, 2025 · 2cf3ffb · 2cf3ffb
1 parent 6d7f24c
commit 2cf3ffb
Showing 1 changed file with 6 additions and 6 deletions.
diff --git 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