let definition2pres ?recno term2pres d =
let name = match d.Content.def_name with Some x -> x|_->assert false in
- let rno = match recno with None -> assert false | Some x -> x in
+ let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
let ty = d.Content.def_type in
let module P = CicNotationPt in
let rec split_pi i t =
if i <= 1 then
match t with
- | P.Binder ((`Pi|`Forall),(var,_ as v),t) -> [v], var, t
+ | P.Binder ((`Pi|`Forall),(var,_ as v),t)
+ | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) ->
+ [v], var, t
| _ -> assert false
else
match t with
- | P.Binder ((`Pi|`Forall), var ,ty) ->
+ | P.Binder ((`Pi|`Forall), var ,ty)
+ | P.AttributedTerm (_, P.Binder ((`Pi|`Forall), var ,ty)) ->
let l, r, t = split_pi (i-1) ty in
var :: l, r, t
| _ -> assert false
in
B.b_hv []
[B.b_hv []
- ([ B.b_space; B.b_text [] name ] @ params @
- [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space;
+ ([ B.b_space; B.b_text [] name; B.b_space ] @ params @
+ (if rno <> -1 then [B.b_kw "on" ; B.b_space; term2pres rec_param ] else [])
+ @[ B.b_space;
B.b_text [] ":"; B.b_space; term2pres ty]);
B.b_text [] ":=";
B.b_h [] [B.b_space;term2pres body] ]