diff options
| author | gareuselesinge | 2013-08-20 12:43:42 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-20 12:43:42 +0000 |
| commit | 645d960c5267b7b79ed0623a494588f7043ccce4 (patch) | |
| tree | 3abcad6e7b33ffaeda507c1356f63f86f2e7b5f4 | |
| parent | 16a2717d25096fcbd07b252e775b66b6fbb6d2bd (diff) | |
Fix STM: Module Import may change the parser
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16714 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernac_classifier.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index ad199b0c7d..099f089c3c 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -140,8 +140,9 @@ let rec classify_vernac e = (* (Local) Notations have to disappear *) | VernacEndSegment _ -> VtSideff [], VtNow (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (_,(_,id),bl,_) - | VernacDefineModule (_,(_,id),bl,_,_) + | VernacDeclareModule (exp,(_,id),bl,_) + | VernacDefineModule (exp,(_,id),bl,_,_) -> + VtSideff [id], if bl = [] && exp = None then VtLater else VtNow | VernacDeclareModuleType ((_,id),bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) |