diff options
Diffstat (limited to 'common/Smallstep.v')
| -rw-r--r-- | common/Smallstep.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/common/Smallstep.v b/common/Smallstep.v index 9c91243a..c269013b 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -786,7 +786,7 @@ End SIMULATION_SEQUENCES. Lemma compose_forward_simulations: forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3. Proof. - intros L1 L2 L3 S12 S23. + intros L1 L2 L3 S12 S23. destruct S12 as [index order match_states props]. destruct S23 as [index' order' match_states' props']. @@ -1632,7 +1632,7 @@ Theorem factor_forward_simulation: forward_simulation L1 L2 -> single_events L2 -> forward_simulation (atomic L1) L2. Proof. - intros L1 L2 FS L2single. + intros L1 L2 FS L2single. destruct FS as [index order match_states sim]. apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor. - (* wf *) @@ -1727,7 +1727,7 @@ Theorem factor_backward_simulation: backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 -> backward_simulation L1 (atomic L2). Proof. - intros L1 L2 BS L1single L2wb. + intros L1 L2 BS L1single L2wb. destruct BS as [index order match_states sim]. apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor. - (* wf *) |