diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 281 |
1 files changed, 139 insertions, 142 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 1e50bc51..21baeb58 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id$ *) open Pp open Util @@ -62,20 +62,20 @@ let with_line_skip p = if ismt p then mt() else (fnl () ++ p) (********************************) (** Printing implicit arguments *) - + let conjugate_to_be = function [_] -> "is" | _ -> "are" let pr_implicit imp = pr_id (name_of_implicit imp) let print_impl_args_by_name max = function | [] -> mt () - | impls -> - hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ - prlist_with_sep pr_coma pr_implicit impls ++ spc() ++ + | impls -> + hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ + prlist_with_sep pr_comma pr_implicit impls ++ spc() ++ str (conjugate_to_be impls) ++ str" implicit" ++ (if max then strbrk " and maximally inserted" else mt())) ++ fnl() -let print_impl_args l = +let print_impl_args l = let imps = List.filter is_status_implicit l in let maximps = List.filter Impargs.maximal_insertion_of imps in let nonmaximps = list_subtract imps maximps in @@ -87,25 +87,25 @@ let print_impl_args l = let print_ref reduce ref = let typ = Global.type_of_global ref in - let typ = + let typ = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ - in it_mkProd_or_LetIn ccl ctx + in it_mkProd_or_LetIn ccl ctx else typ in hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl () let print_argument_scopes = function | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl() | l when not (List.for_all ((=) None) l) -> - hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ + hov 2 (str"Argument scopes are" ++ spc() ++ + str "[" ++ prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ str "]") ++ fnl() | _ -> mt() -let need_expansion impl ref = +let need_expansion impl ref = let typ = Global.type_of_global ref in - let ctx = fst (decompose_prod_assum typ) in + let ctx = (prod_assum typ) in let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in impl <> [] & List.length impl >= nprods & let _,lastimpl = list_chop nprods impl in @@ -116,7 +116,7 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = function - | VarRef v when pi2 (Environ.lookup_named v env) <> None -> + | VarRef v when pi2 (Environ.lookup_named v env) <> None -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v))) | ConstRef cst -> let cb = Environ.lookup_constant cst env in @@ -129,7 +129,7 @@ let opacity env = function let print_opacity ref = match opacity (Global.env()) ref with | None -> mt () - | Some s -> pr_global ref ++ str " is " ++ + | Some s -> pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" | TransparentMaybeOpacified Conv_oracle.Opaque -> @@ -140,14 +140,14 @@ let print_opacity ref = "transparent (with expansion weight "^string_of_int n^")" | TransparentMaybeOpacified Conv_oracle.Expand -> "transparent (with minimal expansion weight)") ++ fnl() - + let print_name_infos ref = let impl = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in - let type_for_implicit = + let type_for_implicit = if need_expansion impl ref then (* Need to reduce since implicits are computed with products flattened *) - str "Expanded type for implicit arguments" ++ fnl () ++ + str "Expanded type for implicit arguments" ++ fnl () ++ print_ref true ref ++ fnl() else mt() in type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes @@ -155,14 +155,14 @@ let print_name_infos ref = let print_id_args_data test pr id l = if List.exists test l then str"For " ++ pr_id id ++ str": " ++ pr l - else + else mt() let print_args_data_of_inductive_ids get test pr sp mipv = prvecti - (fun i mip -> + (fun i mip -> print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) ++ - prvecti + prvecti (fun j idc -> print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1)))) mip.mind_consnames) @@ -173,7 +173,7 @@ let print_inductive_implicit_args = implicits_of_global is_status_implicit print_impl_args let print_inductive_argument_scopes = - print_args_data_of_inductive_ids + print_args_data_of_inductive_ids Notation.find_arguments_scope ((<>) None) print_argument_scopes (*********************) @@ -190,8 +190,8 @@ let locate_any_name ref = let module N = Nametab in let (loc,qid) = qualid_of_reference ref in try Term (N.locate qid) - with Not_found -> - try Syntactic (N.locate_syntactic_definition qid) + with Not_found -> + try Syntactic (N.locate_syndef qid) with Not_found -> try Dir (N.locate_dir qid) with Not_found -> @@ -205,9 +205,9 @@ let pr_located_qualid = function | IndRef _ -> "Inductive" | ConstructRef _ -> "Constructor" | VarRef _ -> "Variable" in - str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref) + str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) | Syntactic kn -> - str "Notation" ++ spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn) + str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) | Dir dir -> let s,dir = match dir with | DirOpenModule (dir,_) -> "Open Module", dir @@ -218,8 +218,8 @@ let pr_located_qualid = function in str s ++ spc () ++ pr_dirpath dir | ModuleType (qid,_) -> - str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid) - | Undefined qid -> + str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid) + | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." let print_located_qualid ref = @@ -228,10 +228,10 @@ let print_located_qualid ref = let expand = function | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref - | SyntacticDef kn -> + | SynDef kn -> Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in - match List.map expand (N.extended_locate_all qid) with - | [] -> + match List.map expand (N.locate_extended_all qid) with + | [] -> let (dir,id) = repr_qualid qid in if dir = empty_dirpath then str "No object of basename " ++ pr_id id @@ -291,7 +291,7 @@ let print_constructors envpar names types = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c) (Array.to_list (array_map2 (fun n t -> (n,t)) names types)) - in + in hv 0 (str " " ++ pc) let build_inductive sp tyi = @@ -300,7 +300,7 @@ let build_inductive sp tyi = let args = extended_rel_list 0 params in let env = Global.env() in let fullarity = match mip.mind_arity with - | Monomorphic ar -> ar.mind_user_arity + | Monomorphic ar -> ar.mind_user_arity | Polymorphic ar -> it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in let arity = hnf_prod_applist env fullarity args in @@ -335,7 +335,7 @@ let get_fields = let id = match na with Name id -> id | Anonymous -> id_of_string "_" in prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c | _ -> List.rev l - in + in prodec_rec [] [] let pr_record (sp,tyi) = @@ -345,15 +345,15 @@ let pr_record (sp,tyi) = let fields = get_fields cstrtypes.(0) in hov 0 ( hov 0 ( - str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ + str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++ - str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ - str ":= " ++ pr_id cstrnames.(0)) ++ + str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ + str ":= " ++ pr_id cstrnames.(0)) ++ brk(1,2) ++ - hv 2 (str "{" ++ - prlist_with_sep (fun () -> str ";" ++ brk(1,0)) - (fun (id,b,c) -> - str " " ++ pr_id id ++ str (if b then " : " else " := ") ++ + hv 2 (str "{ " ++ + prlist_with_sep (fun () -> str ";" ++ brk(2,0)) + (fun (id,b,c) -> + pr_id id ++ str (if b then " : " else " := ") ++ pr_lconstr_env envpar c) fields) ++ str" }") let gallina_print_inductive sp = @@ -364,11 +364,11 @@ let gallina_print_inductive sp = pr_record (List.hd names) else pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ - with_line_skip + with_line_skip (print_inductive_implicit_args sp mipv ++ print_inductive_argument_scopes sp mipv) -let print_named_decl id = +let print_named_decl id = gallina_print_named_decl (Global.lookup_named id) ++ fnl () let gallina_print_section_variable id = @@ -391,26 +391,26 @@ let print_constant with_values sep sp = let val_0 = cb.const_body in let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( - match val_0 with - | None -> - str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + match val_0 with + | None -> + str"*** [ " ++ + print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" - | _ -> + | _ -> print_basename sp ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)) ++ fnl () let gallina_print_constant_with_infos sp = - print_constant true " = " sp ++ + print_constant true " = " sp ++ with_line_skip (print_name_infos (ConstRef sp)) let gallina_print_syntactic_def kn = let sep = " := " and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn - and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in + and (vars,a) = Syntax_def.search_syntactic_definition kn in let c = Topconstr.rawconstr_of_aconstr dummy_loc a in - str "Notation " ++ pr_qualid qid ++ + str "Notation " ++ pr_qualid qid ++ prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++ Constrextern.without_symbols pr_lrawconstr c ++ fnl () @@ -419,42 +419,42 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = and tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes + (* Outside sections, VARIABLES still exist but only with universes constraints *) (try Some(print_named_decl (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> Some (print_constant with_values sep (constant_of_kn kn)) | (_,"INDUCTIVE") -> - Some (gallina_print_inductive kn) + Some (gallina_print_inductive (mind_of_kn kn)) | (_,"MODULE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = repr_kn kn in Some (print_module with_values (MPdot (mp,l))) | (_,"MODULE TYPE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = repr_kn kn in Some (print_modtype (MPdot (mp,l))) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None (* To deal with forgotten cases... *) | (_,s) -> None -let gallina_print_library_entry with_values ent = +let gallina_print_library_entry with_values ent = let pr_name (sp,_) = pr_id (basename sp) in match ent with - | (oname,Lib.Leaf lobj) -> + | (oname,Lib.Leaf lobj) -> gallina_print_leaf_entry with_values (oname,lobj) - | (oname,Lib.OpenedSection (dir,_)) -> + | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> + | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary (dir,_)) -> Some (str " >>>>>>> Library " ++ pr_dirpath dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> + | (oname,Lib.ClosedModule _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) | (oname,Lib.OpenedModtype _) -> Some (str " >>>>>>> Module Type " ++ pr_name oname) - | (oname,Lib.ClosedModtype _) -> + | (oname,Lib.ClosedModtype _) -> Some (str " >>>>>>> Closed Module Type " ++ pr_name oname) | (_,Lib.FrozenState _) -> None @@ -464,14 +464,14 @@ let gallina_print_leaf_entry with_values c = | None -> mt () | Some pp -> pp ++ fnl() -let gallina_print_context with_values = +let gallina_print_context with_values = let rec prec n = function - | h::rest when n = None or Option.get n > 0 -> + | h::rest when n = None or Option.get n > 0 -> (match gallina_print_library_entry with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () - in + in prec let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} = @@ -520,16 +520,16 @@ let print_typed_value x = print_typed_value_in_env (Global.env ()) x let print_judgment env {uj_val=trm;uj_type=typ} = print_typed_value_in_env env (trm, typ) - + let print_safe_judgment env j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in print_typed_value_in_env env (trm, typ) - + (*********************) (* *) -let print_full_context () = +let print_full_context () = print_context true None (Lib.contents_after None) let print_full_context_typ () = @@ -540,33 +540,34 @@ let print_full_pure_context () = | ((_,kn),Lib.Leaf lobj)::rest -> let pp = match object_tag lobj with | "CONSTANT" -> - let con = constant_of_kn kn in + let con = Global.constant_of_delta (constant_of_kn kn) in let cb = Global.lookup_constant con in let val_0 = cb.const_body in let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( - match val_0 with + match val_0 with | None -> str (if cb.const_opaque then "Axiom " else "Parameter ") ++ print_basename con ++ str " : " ++ cut () ++ pr_ltype typ | Some v -> if cb.const_opaque then - str "Theorem " ++ print_basename con ++ cut () ++ + str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ str "Proof " ++ print_body val_0 else - str "Definition " ++ print_basename con ++ cut () ++ + str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ print_body val_0) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> - let (mib,mip) = Global.lookup_inductive (kn,0) in + let mind = Global.mind_of_delta (mind_of_kn kn) in + let (mib,mip) = Global.lookup_inductive (mind,0) in let mipv = mib.mind_packets in - let names = list_tabulate (fun x -> (kn,x)) (Array.length mipv) in - pr_mutual_inductive mib.mind_finite names ++ str "." ++ + let names = list_tabulate (fun x -> (mind,x)) (Array.length mipv) in + pr_mutual_inductive mib.mind_finite names ++ str "." ++ fnl () ++ fnl () | "MODULE" -> (* TODO: make it reparsable *) - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = repr_kn kn in print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | "MODULE TYPE" -> (* TODO: make it reparsable *) @@ -576,7 +577,7 @@ let print_full_pure_context () = | _ -> mt () in prec rest ++ pp | _::rest -> prec rest - | _ -> mt () in + | _ -> mt () in prec (Lib.contents_after None) (* For printing an inductive definition with @@ -584,14 +585,14 @@ let print_full_pure_context () = assume that the declaration of constructors and eliminations follows the definition of the inductive type *) -let list_filter_vec f vec = - let rec frec n lf = - if n < 0 then lf - else if f vec.(n) then +let list_filter_vec f vec = + let rec frec n lf = + if n < 0 then lf + else if f vec.(n) then frec (n-1) (vec.(n)::lf) - else + else frec (n-1) lf - in + in frec (Array.length vec -1) [] (* This is designed to print the contents of an opened section *) @@ -608,19 +609,18 @@ let read_sec_context r = error "Cannot print the contents of a closed section." (* LEM: Actually, we could if we wanted to. *) | [] -> [] - | hd::rest -> get_cxt (hd::in_cxt) rest + | hd::rest -> get_cxt (hd::in_cxt) rest in let cxt = (Lib.contents_after None) in List.rev (get_cxt [] cxt) -let print_sec_context sec = +let print_sec_context sec = print_context true None (read_sec_context sec) let print_sec_context_typ sec = print_context false None (read_sec_context sec) -let print_name ref = - match locate_any_name ref with +let print_any_name = function | Term (ConstRef sp) -> print_constant_with_infos sp | Term (IndRef (sp,_)) -> print_inductive sp | Term (ConstructRef ((sp,_),_)) -> print_inductive sp @@ -631,49 +631,44 @@ let print_name ref = | ModuleType (_,kn) -> print_modtype kn | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) - let dir,str = repr_qualid qid in + let dir,str = repr_qualid qid in if (repr_dirpath dir) <> [] then raise Not_found; - let (_,c,typ) = Global.lookup_named str in + let (_,c,typ) = Global.lookup_named str in (print_named_decl (str,c,typ)) with Not_found -> - try - let sp = Nametab.locate_obj qid in - let (oname,lobj) = - let (oname,entry) = - List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None) - in - match entry with - | Lib.Leaf obj -> (oname,obj) - | _ -> raise Not_found - in - print_leaf_entry true (oname,lobj) - with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_opaque_name qid = +let print_name = function + | Genarg.ByNotation (loc,ntn,sc) -> + print_any_name + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + ntn sc)) + | Genarg.AN ref -> + print_any_name (locate_any_name ref) + +let print_opaque_name qid = let env = Global.env () in match global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if cb.const_body <> None then print_constant_with_infos cst - else + else error "Not a defined constant." | IndRef (sp,_) -> print_inductive sp - | ConstructRef cstr -> + | ConstructRef cstr -> let ty = Inductiveops.type_of_constructor env cstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let (_,c,ty) = lookup_named id env in + let (_,c,ty) = lookup_named id env in print_named_decl (id,c,ty) -let print_about ref = - let k = locate_any_name ref in +let print_about_any k = begin match k with | Term ref -> - print_ref false ref ++ fnl () ++ print_name_infos ref ++ + print_ref false ref ++ fnl () ++ print_name_infos ref ++ print_opacity ref | Syntactic kn -> print_syntactic_def kn @@ -682,26 +677,34 @@ let print_about ref = ++ hov 0 (str "Expands to: " ++ pr_located_qualid k) +let print_about = function + | Genarg.ByNotation (loc,ntn,sc) -> + print_about_any + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + ntn sc)) + | Genarg.AN ref -> + print_about_any (locate_any_name ref) + let print_impargs ref = - let ref = Nametab.global ref in + let ref = Smartlocate.smart_global ref in let impl = implicits_of_global ref in let has_impl = List.filter is_status_implicit impl <> [] in (* Need to reduce since implicits are computed with products flattened *) print_ref (need_expansion impl ref) ref ++ fnl() ++ - (if has_impl then print_impl_args impl + (if has_impl then print_impl_args impl else (str "No implicit arguments" ++ fnl ())) -let unfold_head_fconst = +let unfold_head_fconst = let rec unfrec k = match kind_of_term k with - | Const cst -> constant_value (Global.env ()) cst + | Const cst -> constant_value (Global.env ()) cst | Lambda (na,t,b) -> mkLambda (na,t,unfrec b) | App (f,v) -> appvect (unfrec f,v) | _ -> k - in + in unfrec (* for debug *) -let inspect depth = +let inspect depth = print_context false (Some depth) (Lib.contents_after None) @@ -715,8 +718,8 @@ let print_coercion_value v = pr_lconstr (get_coercion_value v) let print_class i = let cl,_ = class_info_from_index i in pr_class cl - -let print_path ((i,j),p) = + +let print_path ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ @@ -724,45 +727,39 @@ let print_path ((i,j),p) = let _ = Classops.install_path_printer print_path -let print_graph () = +let print_graph () = prlist_with_sep pr_fnl print_path (inheritance_graph()) -let print_classes () = +let print_classes () = prlist_with_sep pr_spc pr_class (classes()) -let print_coercions () = +let print_coercions () = prlist_with_sep pr_spc print_coercion_value (coercions()) - + let index_of_class cl = - try + try fst (class_info cl) - with _ -> + with _ -> errorlabstrm "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between cls clt = let i = index_of_class cls in let j = index_of_class clt in - let p = - try - lookup_path_between_class (i,j) - with _ -> + let p = + try + lookup_path_between_class (i,j) + with _ -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in print_path ((i,j),p) -let pr_cs_pattern = function - Const_cs c -> pr_global c - | Prod_cs -> str "_ -> _" - | Default_cs -> str "_" - | Sort_cs s -> pr_sort_family s - let print_canonical_projections () = - prlist_with_sep pr_fnl - (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ - str " <- " ++ + prlist_with_sep pr_fnl + (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ + str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") (canonical_projections ()) @@ -773,25 +770,25 @@ let print_canonical_projections () = open Typeclasses -let pr_typeclass env t = +let pr_typeclass env t = print_ref false t.cl_impl let print_typeclasses () = let env = Global.env () in prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) - -let pr_instance env i = + +let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) - print_ref false (ConstRef (instance_impl i)) - + print_ref false (instance_impl i) + let print_all_instances () = let env = Global.env () in - let inst = all_instances () in + let inst = all_instances () in prlist_with_sep fnl (pr_instance env) inst let print_instances r = let env = Global.env () in - let inst = instances r in + let inst = instances r in prlist_with_sep fnl (pr_instance env) inst - + |