diff options
Diffstat (limited to 'lib/Iteration.v')
| -rw-r--r-- | lib/Iteration.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Iteration.v b/lib/Iteration.v index 235b650..1c3c9cc 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -171,7 +171,7 @@ Proof. intros. unfold iter in H1. rewrite unroll_Fix in H1. unfold iter_step in H1. destruct (peq x 1). discriminate. specialize (step_prop a H0). - destruct (step a) as [b'|a']_eqn. + destruct (step a) as [b'|a'] eqn:?. inv H1. auto. apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto. Qed. |