diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cminorgenproof.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ea1bc89c..a6d58f17 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -20,7 +20,7 @@ Require Import AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Csharpminor Switch Cminor Cminorgen. -Open Local Scope error_monad_scope. +Local Open Scope error_monad_scope. Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) := match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index aeb31fe2..792a73f9 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -24,8 +24,8 @@ Require Import Coqlib Maps Errors Integers Floats. Require Import AST Linking. Require Import Ctypes Cop Clight Cminor Csharpminor. -Open Local Scope string_scope. -Open Local Scope error_monad_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. (** * Csharpminor constructors *) |