diff options
| author | herbelin | 2005-12-23 10:43:37 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-23 10:43:37 +0000 |
| commit | 29b75ca42b7824f5feec24df5ecc7cd75cb78251 (patch) | |
| tree | 7b292623378acfb1c70cb692ba4a13290381eeef /contrib/interface/parse.ml | |
| parent | c506c385473224345526bfff4b71c56222ccbb11 (diff) | |
Simplifification de vernac_expr li l'abandon du traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |