- Module/Declare Module syntax made more uniform:

  * "Module X [binders] [:T] [:= b]." is now used to define a module both
    in module definitions and module type definitions. Moreover "b" can now
    be a functor application in every situation (this was not accepted for
    module definitions in module type definitions)
  * "Declare Module X : T." is now used to declare a module both in module
    definitions and module type definitions.
- Added syntactic sugar "Declare Module Export/Import" and
  "Module Export/Import"
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
  "Module Type M(Export/Import X Y: T)"
  (only for interactive definitions) (doc TODO)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 4 insertions, 4 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index b171aab6b7..0a72c97bc4 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -329,8 +329,8 @@ type reset_info = NoReset | Reset of Names.identifier * bool ref
 let compute_reset_info = function 
   | VernacDefinition (_, (_,id), DefineBody _, _) 
   | VernacBeginSection (_,id) 
-  | VernacDefineModule ((_,id), _, _, _) 
-  | VernacDeclareModule ((_,id), _, _, _)
+  | VernacDefineModule (_,(_,id), _, _, _) 
+  | VernacDeclareModule (_,(_,id), _, _)
   | VernacDeclareModuleType ((_,id), _, _)
   | VernacAssumption (_, (_,((_,id)::_,_))::_)
   | VernacInductive (_, ((_,id),_,_,_,_) :: _) ->
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 11af7ada6b..bd06c0b07d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -518,8 +518,8 @@ let update_on_end_of_proof id =
 let update_on_end_of_segment id =
   let lookup_section = function 
     | { ast = _, ( VernacBeginSection id'
-		 | VernacDefineModule (id',_,_,None)
-		 | VernacDeclareModule (id',_,_,None)
+		 | VernacDefineModule (_,id',_,_,None)
+		 | VernacDeclareModule (_,id',_,_)
 		 | VernacDeclareModuleType (id',_,None)); 
 	reset_info = Reset (_, r) } 
        when id = id' -> raise Exit