renaming

_CoqProject

@@ -26,7 +26,9 @@ theories/sim/program.v
 theories/sim/sflib.v
 theories/sim/instance.v
 theories/sim/body.v
-theories/sim/one_step.v
+theories/sim/refl_step.v
+theories/sim/left_step.v
+theories/sim/right_step.v
 theories/opt/ex1.v
 theories/opt/ex1_2.v
 theories/opt/ex2.v

theories/opt/ex1.v

-From stbor.sim Require Import local invariant one_step.
+From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 

theories/opt/ex1_2.v

-From stbor.sim Require Import local invariant one_step.
+From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 

theories/opt/ex2.v

-From stbor.sim Require Import local invariant one_step.
+From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 

theories/opt/ex2_2.v

-From stbor.sim Require Import local invariant one_step.
+From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 

theories/sim/program.v

 From stbor.lang Require Import steps_wf steps_inversion.
-From stbor.sim Require Import sflib behavior global local invariant global_adequacy local_adequacy one_step.
+From stbor.sim Require Import sflib behavior global local invariant.
+From stbor.sim Require Import global_adequacy local_adequacy refl_step.
 
 Set Default Proof Using "Type".