aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--backend/Selection.v4
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