let r2s pp_fix_name r =
try
match r with
- | R.Ref (_,u,R.Ind i) ->
- (match snd(NCicEnvironment.get_obj u) with
+ | R.Ref (_,u,R.Ind (_,i)) ->
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,name,_,_ = List.nth itl i in name
| _ -> assert false)
| R.Ref (_,u,R.Con (i,j)) ->
- (match snd(NCicEnvironment.get_obj u) with
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,_,_,cl = List.nth itl i in
let _,name,_ = List.nth cl (j-1) in name
| _ -> assert false)
| R.Ref (_,u,(R.Decl | R.Def )) ->
- (match snd(NCicEnvironment.get_obj u) with
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Constant (_,name,_,_,_) -> name
| _ -> assert false)
| R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
- (match snd(NCicEnvironment.get_obj u) with
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Fixpoint (_,fl,_) ->
if pp_fix_name then
let _,name,_,_,_ = List.nth fl i in name
let ppobj = function
| (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
"{"^NUri.string_of_uri u^"}\n"^
- "let rec "^
+ (if b then "let rec " else "let corec ") ^
String.concat "\nand "
(List.map (fun (_,name,n,ty,bo) ->
name^ " on " ^ string_of_int n ^ " : " ^
ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
;;
+
+let rec ppcontext ~subst ~metasenv = function
+ | [] -> ""
+ | (name, NCic.Decl t) :: tl ->
+ ppcontext ~subst ~metasenv tl ^
+ name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl t ^ "\n"
+ | (name, NCic.Def (bo,ty)) :: tl->
+ ppcontext ~subst ~metasenv tl ^
+ name ^ ": " ^ ppterm ~subst ~metasenv ~context:tl ty ^
+ " := " ^ ppterm ~subst ~metasenv ~context:tl bo ^ "\n"
+;;