Romain Beguet faa8012473 Make has_spark_mode_on and is_subject_to_proof available on any node. ...

This also modifies the previous implementation by always propagating the
`include_skip_proof_annotations` flag, whereas previously some of the
internal properties would "forget" about it, for example the one on
DeclarativePart.

However it seems necessary to propagate the flag to correctly handle
`is_subject_to_proof` on local declarative parts nested in a subprogram
annotated with Skip_Proof.

2024-03-25 11:28:20 +01:00

5.4 KiB

Executable File

Raw Permalink Blame History

View Raw