let ppid =
let reserved =
[ "to";
- "mod"
+ "mod";
+ "val"
]
in
function n ->
let rec args context =
function
Cic.Prod (n,s,t) ->
+ let n =
+ match n with
+ Cic.Anonymous -> Cic.Anonymous
+ | Cic.Name n -> Cic.Name (String.uncapitalize n)
+ in
(match analyze_type context s with
`Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
| `Statement
(* ppinductiveType (typename, inductive, arity, cons) *)
(* pretty-prints a single inductive definition *)
(* (typename, inductive, arity, cons) *)
-let ppinductiveType current_module_name (typename, inductive, arity, cons) =
+let ppinductiveType current_module_name nparams (typename, inductive, arity, cons)
+=
match analyze_type [] arity with
`Sort Cic.Prop -> ""
| `Statement
else (
let abstr,scons =
List.fold_right
- (fun (id,ty) (abstr,i) ->
+ (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
let abstr',sargs = ppty current_module_name [] ty in
let sargs = String.concat " * " sargs in
- abstr'@abstr,
+ abstr',
String.capitalize id ^
(if sargs = "" then "" else " of " ^ sargs) ^
(if i = "" then "" else "\n | ") ^ i)
pp ~metasenv:conjectures ty []
| C.InductiveDefinition (l, params, nparams, _) ->
List.fold_right
- (fun x i -> ppinductiveType current_module_name x ^ i) l ""
+ (fun x i -> ppinductiveType current_module_name nparams x ^ i) l ""
;;
let ppobj current_module_name obj =