aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml4')
-rw-r--r--parsing/pcoq.ml413
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