Modules dans COQ\!\!\!\!

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

1 files changed, 13 insertions, 0 deletions

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d26613b10..2d444fcbb 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -222,6 +222,7 @@ let create_univ s =
 
 let uprim   = create_univ "prim"
 let uconstr = create_univ "constr"
+let umodule = create_univ "module"
 let utactic = create_univ "tactic"
 let uvernac = create_univ "vernac"
 
@@ -398,6 +399,18 @@ module Constr =
   end
 
 
+module Module =
+  struct
+    let gec = make_entry umodule inPureAstType
+    let gec_list = make_entry umodule inAstListType
+
+    let ident = gec "ident"
+    let qualid = gec_list "qualid"
+    let ne_binders_list = gec_list "ne_binders_list"
+    let module_expr = gec "module_expr"
+    let module_type = gec "module_type"
+  end
+
 module Tactic =
   struct
     let gec = make_entry utactic inPureAstType