diff options
Diffstat (limited to 'src/hls/DeadBlocksproof.v')
| -rw-r--r-- | src/hls/DeadBlocksproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v index 7f1da9c..107e206 100644 --- a/src/hls/DeadBlocksproof.v +++ b/src/hls/DeadBlocksproof.v @@ -544,7 +544,7 @@ Proof. elim H. intros. - elim not_seen_sons_prop6 with (1:=TT) (i0:=i); auto with datatypes. + eelim not_seen_sons_prop6 with (1:=TT) (i:=i); auto with datatypes. rewrite PTree.gsspec; destruct peq; subst; intros; auto with datatypes. rewrite PTree.gempty in H0; congruence. |