let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
let rex = Str.regexp ("^"^ident^"$") in
if Str.string_match rex id 0 then
- let rex = Str.regexp
- ("^\\(cic:/\\|theory:/\\)"^ident^
- "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
- "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$")
- in
- if Str.string_match rex uri 0 then
+ if (try ignore (UriManager.uri_of_string uri); true
+ with UriManager.IllFormedUri _ -> false)
+ then
TacticAst.Ident_alias (id, uri)
else
raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))
TacticAst.Set (loc, n, v)
| [ IDENT "drop" ] -> TacticAst.Drop loc
| [ IDENT "qed" ] -> TacticAst.Qed loc
+ | IDENT "variant" ; name = IDENT; SYMBOL ":";
+ typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
+ TacticAst.Obj (loc,
+ TacticAst.Theorem
+ (`Variant,name,typ,Some (CicAst.Ident (newname, None))))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))