diff options
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index ff3d827d9..26c76e594 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -106,7 +106,7 @@ let execute_when_necessary ast = let execute_when_necessary v = (match v with | VernacGrammar _ -> Vernacentries.interp v - | VernacOpenScope sc -> Vernacentries.interp v + | VernacOpenCloseScope sc -> Vernacentries.interp v | VernacRequire (_,_,l) -> (try Vernacentries.interp v |