diff options
author | 2010-07-21 09:46:51 +0200 | |
---|---|---|
committer | 2010-07-21 09:46:51 +0200 | |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /parsing/g_prim.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
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]) ] ] |