%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%start main
-%type <((string * CicTextualParser0.uri) -> unit) -> (string list * ((string -> CicTextualParser0.uri option) -> Cic.term)) option> main
+%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
%%
main:
- expr { function _ -> Some $1 }
- | alias { function register -> register $1 ; None }
- | EOF { raise CicTextualParser0.Eof }
+ expr EOF { $1 }
;
expr2:
CONURI exp_named_subst
{ let dom,mk_exprsubstitutionlist = $3 in
dom, function interp -> None::(mk_exprsubstitutionlist interp)
}
-;
-alias:
- ALIAS ID CONURI
- { $2,(CicTextualParser0.ConUri $3) }
- | ALIAS ID VARURI
- { $2,(CicTextualParser0.VarUri $3) }
- | ALIAS ID INDTYURI
- { $2,(CicTextualParser0.IndTyUri (fst $3, snd $3)) }
- | ALIAS ID INDCONURI
- { let uri,indno,consno = $3 in
- $2,(CicTextualParser0.IndConUri (uri, indno, consno))
- }