let module CTP0 = CicTextualParser0 in
match interp id with
None -> raise (UnknownIdentifier id)
- | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno)) -> (uri,tyno)
+ | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
| Some _ -> raise InductiveTypeURIExpected
;;
%token <UriManager.uri> VARURI
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> INDCONURI
-%token ALIAS
%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
%%
main:
- expr EOF { $1 }
+ | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
+ | expr EOF { $1 }
+ | expr SEMICOLON { $1 } /* FG: to read several terms in a row
+ * Do we need to clear some static variables?
+ */
;
expr2:
CONURI exp_named_subst