let mk_rec_corec ind_kind defs loc =
let name,ty =
match defs with
- | (params,(N.Ident (name, None), ty),_,_) :: _ ->
+ | (params,(N.Ident (name, `Ambiguous), ty),_,_) :: _ ->
let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
let ty =
List.fold_right
name,ty
| _ -> assert false
in
- let body = N.Ident (name,None) in
+ let body = N.Ident (name,`Ambiguous) in
(loc, N.Theorem(`Definition, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
let nmk_rec_corec ind_kind defs loc =
(params,name,typ,fields)
] ];
+ (* XXX: alias spec must be revised (no more instance nums) *)
alias_spec: [
[ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
let alpha = "[a-zA-Z]" in
let instance =
match instance with Some i -> i | None -> 0
in
- G.Symbol_alias (symbol, instance, dsc)
+ G.Symbol_alias (symbol, None, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- G.Number_alias (instance, dsc)
+ G.Number_alias (None,dsc)
]
];
argument: [