diff options
Diffstat (limited to 'lib/Parmov.v')
| -rw-r--r-- | lib/Parmov.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Parmov.v b/lib/Parmov.v index 493b0bd..fb04310 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -1017,7 +1017,7 @@ Lemma split_move_charact: Proof. unfold no_read. intros m r. functional induction (split_move m r). red; simpl. tauto. - rewrite _x. split. reflexivity. simpl;auto. + split. reflexivity. simpl; auto. rewrite e1 in IHo. simpl. intuition. rewrite e1 in IHo. destruct IHo. split. rewrite H. reflexivity. simpl. intuition. |