diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 1c9e1e46b..6b5d03d91 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -273,6 +273,8 @@ module Prim = let bigint = Gram.Entry.create "Prim.bigint" let string = gec_gen rawwit_string "string" let reference = make_gen_entry uprim rawwit_ref "reference" + let by_notation = Gram.Entry.create "by_notation" + let smart_global = Gram.Entry.create "smart_global" (* parsed like ident but interpreted as a term *) let var = gec_gen rawwit_var "var" |