- let abstr,scons =
- List.fold_right
- (fun (id,ty) (abstr,i) ->
- let rec args context =
- function
- Cic.Prod (n,s,t) ->
- (match analyze_type context s with
- `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
- | `Statement
- | `Sort _ ->
- let n =
- match n with
- Cic.Anonymous -> Cic.Anonymous
- | Cic.Name name -> Cic.Name ("'" ^ name) in
- let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
- (match n with
- Cic.Anonymous -> abstr
- | Cic.Name name -> name::abstr),
- args
- | `Type ->
- let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
- abstr,pp current_module_name s context::args)
- | _ -> [],[]
+ match analyze_type [] arity with
+ `Sort Cic.Prop -> ""
+ | `Statement
+ | `Type -> assert false
+ | `Sort _ ->
+ let abstr,scons =
+ List.fold_right
+ (fun (id,ty) (abstr,i) ->
+ let abstr',sargs = ppty current_module_name [] ty in
+ let sargs = String.concat " * " sargs in
+ abstr'@abstr,
+ String.capitalize id ^
+ (if sargs = "" then "" else " of " ^ sargs) ^
+ (if i = "" then "\n" else "\n | ") ^ i)
+ cons ([],"")