| IDENT "timeout"
| IDENT "library"
| IDENT "type"
- | IDENT "steps"
| IDENT "all"
]
];
let rex = Str.regexp ("^"^ident^"$") in
if Str.string_match rex id 0 then
if (try ignore (UriManager.uri_of_string uri); true
- with UriManager.IllFormedUri _ -> false)
+ with UriManager.IllFormedUri _ -> false) ||
+ (try ignore (NReference.reference_of_string uri); true
+ with NReference.IllFormedReference _ -> false)
then
L.Ident_alias (id, uri)
- else
+ else
raise
(HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
else
indty = tactic_term; paramspec = inverter_param_list ->
G.Inverter
(loc, name, indty, paramspec)
- | IDENT "record" ; (params,name,ty,fields) = record_spec ->
+ | IDENT "record" ; (params,name,ty,fields) = record_spec ->
G.Obj (loc, N.Record (params,name,ty,fields))
+ | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
+ G.NObj (loc, N.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
G.Default (loc,what,uris)