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