Pretty-printing of Clight uses wrong subscopes

[andrew-appel]

This line of Clightnotations.v does not work properly,

Notation "'for' ( s1 ; e ; s2 ) { s3 }" := (Sfor s1%print_stmt_for e%expr s3%C s2%print_stmt_for) ... : C_scope.

and the reason is Coq bug 8805.

The consequence of the bug is that an extra semicolon printed after s1, because Coq interprets s1 in C_scope instead of in print_stmt_for_scope as it should. Refer to these two lines of Clightnotations.v:

Notation "id = e2" := (Sset id%positive e2%expr) ... : print_stmt_for_scope.
Notation "id = e2 ;" := (Sset id%positive e2%expr) ... : C_scope.

The Coq issue report suggests this will likely be fixed in Coq version 8.10.

[andrew-appel]

It is not yet fixed in Coq 8.11.

[andrew-appel]

Still not fixed in Coq 8.18.