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 =
| _ ->
(*CSC: new NCicPp.status is the best I can do here without changing the
result type *)
- raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term (new NCicPp.status) params)) ]
+ raise (Invalid_argument ("malformed target parameter list 2\n" ^
+ NotationPp.pp_term (new NCicPp.status None ) params)) ]
];
direction: [
[ SYMBOL ">" -> `LeftToRight
(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: [
method parser_db: db
end
-class virtual status =
+class virtual status uid =
object(self)
- inherit CicNotationParser.status ~keywords:[]
+ inherit CicNotationParser.status uid ~keywords:[]
val mutable db = None (* mutable only to initialize it :-( *)
method parser_db = match db with None -> assert false | Some x -> x
method set_parser_db v = {< db = Some v >}
;;
-let parse_statement status =
+let parse_statement status =
+ status#reset_loctable ();
parse_statement status#parser_db
(* vim:set foldmethod=marker: *)