diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-11-25 15:22:07 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-12-08 15:30:58 +0100 |
| commit | e5d132537bd2dbbf9c3d4b313c6b312b62ac133e (patch) | |
| tree | 23798fdb93d0399edfb2d715a9ecb94b92252f23 | |
| parent | 5be9ae2235b16239f023a36679b7d515dd774c68 (diff) | |
| download | compcert-e5d132537bd2dbbf9c3d4b313c6b312b62ac133e.tar.gz compcert-e5d132537bd2dbbf9c3d4b313c6b312b62ac133e.zip | |
Update doc comment
| -rw-r--r-- | backend/Selection.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 8dfe29ef..ca1f1619 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -337,8 +337,8 @@ Definition sel_switch_long := (** Recognition of "then" and "else" statements that support if-conversion. Basically we are interested in assignments to local variables [id = e]. - However the front-end may have put [skip] statements around these - assignments. *) + However the front-end may have put [skip] statements and debug annotations + around these assignments. *) Inductive stmt_class : Type := | SCskip |