diff options
Diffstat (limited to 'parsing/g_prim.ml4')
| -rw-r--r-- | parsing/g_prim.ml4 | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 76225d77..6e7acd3f 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(*i $Id: g_prim.ml4 11525 2008-10-30 22:18:54Z amahboub $ i*) +(*i $Id$ i*) open Pcoq open Names @@ -34,10 +34,10 @@ let my_int_of_string loc s = Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") GEXTEND Gram - GLOBAL: + GLOBAL: bigint natural integer identref name ident var preident - fullyqualid qualid reference dirpath - ne_string string pattern_ident pattern_identref; + fullyqualid qualid reference dirpath ne_lstring + ne_string string pattern_ident pattern_identref by_notation smart_global; preident: [ [ s = IDENT -> s ] ] ; @@ -45,7 +45,7 @@ GEXTEND Gram [ [ s = IDENT -> id_of_string s ] ] ; pattern_ident: - [ [ LEFTQMARK; id = ident -> id ] ] + [ [ s = LEFTQMARK; id = ident -> id ] ] ; pattern_identref: [ [ id = pattern_ident -> (loc, id) ] ] @@ -71,7 +71,7 @@ GEXTEND Gram ; basequalid: [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> make_short_qualid id + | id = ident -> qualid_of_ident id ] ] ; name: @@ -84,14 +84,24 @@ GEXTEND Gram | id = ident -> Ident (loc,id) ] ] ; + by_notation: + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ] + ; + smart_global: + [ [ c = reference -> Genarg.AN c + | ntn = by_notation -> Genarg.ByNotation ntn ] ] + ; qualid: [ [ qid = basequalid -> loc, qid ] ] ; ne_string: - [ [ s = STRING -> + [ [ s = STRING -> if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s ] ] ; + ne_lstring: + [ [ s = ne_string -> (loc,s) ] ] + ; dirpath: [ [ id = ident; l = LIST0 field -> make_dirpath (l@[id]) ] ] |