diff options
Diffstat (limited to 'export')
-rw-r--r-- | export/Clightdefs.v | 2 | ||||
-rw-r--r-- | export/Csyntaxdefs.v | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/export/Clightdefs.v b/export/Clightdefs.v index dc4e3491..3a9da8f6 100644 --- a/export/Clightdefs.v +++ b/export/Clightdefs.v @@ -49,6 +49,8 @@ Definition mkprogram (types: list composite_definition) (** ** Notations *) +Declare Scope clight_scope. + Module ClightNotations. (** A convenient notation [$ "ident"] to force evaluation of diff --git a/export/Csyntaxdefs.v b/export/Csyntaxdefs.v index 84ce9f3a..67bc7f51 100644 --- a/export/Csyntaxdefs.v +++ b/export/Csyntaxdefs.v @@ -49,6 +49,8 @@ Definition mkprogram (types: list composite_definition) (** ** Notations *) +Declare Scope csyntax_scope. + Module CsyntaxNotations. (** A convenient notation [$ "ident"] to force evaluation of |