From 645d960c5267b7b79ed0623a494588f7043ccce4 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Tue, 20 Aug 2013 12:43:42 +0000
Subject: 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
---
 toplevel/vernac_classifier.ml | 5 +++--
 1 file 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 *)
-- 
cgit v1.2.3