diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 40 | ||||
| -rw-r--r-- | printing/printmod.ml | 52 |
2 files changed, 46 insertions, 46 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 10a31ac256..a85e268306 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -304,10 +304,10 @@ let pr_rel_decl env sigma decl = let pbody = match decl with | RelDecl.LocalAssum _ -> mt () | RelDecl.LocalDef (_,c,_) -> - (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in - let pb = if isCast c then surround pb else pb in - (str":=" ++ spc () ++ pb ++ spc ()) in + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = pr_ltype_env env sigma typ in match na with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -329,7 +329,7 @@ let pr_var_list_decl env sigma decl = let pr_named_context env sigma ne_context = hv 0 (Context.Named.fold_outside - (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) + (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) ne_context ~init:(mt ())) let pr_rel_context env sigma rel_context = @@ -436,7 +436,7 @@ let pr_predicate pr_elt (b, elts) = let pr_elts = prlist_with_sep spc pr_elt elts in if b then str"all" ++ - (if List.is_empty elts then mt () else str" except: " ++ pr_elts) + (if List.is_empty elts then mt () else str" except: " ++ pr_elts) else if List.is_empty elts then str"none" else pr_elts @@ -565,10 +565,10 @@ let pr_subgoal n sigma = let rec prrec p = function | [] -> user_err Pp.(str "No such goal.") | g::rest -> - if Int.equal p 1 then + if Int.equal p 1 then pr_selected_subgoal (int n) sigma g - else - prrec (p-1) rest + else + prrec (p-1) rest in prrec n @@ -736,7 +736,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map pr_goal ~diffs ?og_s { it = g ; sigma = sigma } ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l - else + else pr_rec 1 (g::l) in let pr_evar_info gl sigma seeds = @@ -792,15 +792,15 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> - Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); - fnl () + Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); + fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> - Feedback.msg_info (str "All the remaining goals are on the shelf."); - fnl () + Feedback.msg_info (str "All the remaining goals are on the shelf."); + fnl () ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf - | _ , _, _ -> + | _ , _, _ -> let cmd = if quiet then None else Some (str "This subproof is complete, but there are some unfocused goals." ++ @@ -809,8 +809,8 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = fnl ()) in pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals - end - | _ -> + end + | _ -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in @@ -981,17 +981,17 @@ let pr_assumptionset env sigma s = let tran = safe_pr_constant env kn ++ safe_pr_ltype env sigma typ in (v, a, o, tran :: tr) in - let (vars, axioms, opaque, trans) = + let (vars, axioms, opaque, trans) = ContextObjectMap.fold fold s ([], [], [], []) in let theory = if is_impredicative_set env then - [str "Set is impredicative"] + [str "Set is impredicative"] else [] in let theory = if type_in_type env then - str "Type hierarchy is collapsed (logic is inconsistent)" :: theory + str "Type hierarchy is collapsed (logic is inconsistent)" :: theory else theory in let opt_list title = function diff --git a/printing/printmod.ml b/printing/printmod.ml index 4cc6bc2052..85bb287c22 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -63,9 +63,9 @@ let get_new_id locals id = let rec get_id l id = let dir = DirPath.make [id] in if not (Nametab.exists_dir dir) then - id + id else - get_id (Id.Set.add id l) (Namegen.next_ident_away id l) + get_id (Id.Set.add id l) (Namegen.next_ident_away id l) in let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in get_id avoid id @@ -205,10 +205,10 @@ let print_kn locals kn = pr_qualid qid with Not_found -> - try - print_local_modpath locals kn - with - Not_found -> print_modpath locals kn + try + print_local_modpath locals kn + with + Not_found -> print_modpath locals kn let nametab_register_dir obj_mp = let id = mk_fake_top () in @@ -234,11 +234,11 @@ let nametab_register_body mp dir (l,body) = | SFBmind mib -> let mind = MutInd.make2 mp l in Array.iteri - (fun i mip -> + (fun i mip -> push mip.mind_typename (GlobRef.IndRef (mind,i)); Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1))) - mip.mind_consnames) - mib.mind_packets + mip.mind_consnames) + mib.mind_packets type mod_ops = { import_module : export:bool -> ModPath.t -> unit @@ -285,22 +285,22 @@ let print_body is_impl extent env mp (l,body) = | SFBconst cb -> let ctx = Declareops.constant_polymorphic_context cb in (match cb.const_body with - | Def _ -> def "Definition" ++ spc () - | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () - | _ -> def "Parameter" ++ spc ()) ++ name ++ + | Def _ -> def "Definition" ++ spc () + | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () + | _ -> def "Parameter" ++ spc ()) ++ name ++ (match extent with | OnlyNames -> mt () | WithContents -> let bl = UnivNames.universe_binders_with_opt_names ctx None in let sigma = Evd.from_ctx (UState.of_binders bl) in - str " :" ++ spc () ++ + str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ - (match cb.const_body with - | Def l when is_impl -> - spc () ++ - hov 2 (str ":= " ++ + (match cb.const_body with + | Def l when is_impl -> + spc () ++ + hov 2 (str ":= " ++ Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) - | _ -> mt ()) ++ str "." ++ + | _ -> mt ()) ++ str "." ++ Printer.pr_abstract_universe_ctx sigma ctx) | SFBmind mib -> match extent with @@ -314,7 +314,7 @@ let print_body is_impl extent env mp (l,body) = | BiFinite -> def "Variant" | CoFinite -> def "CoInductive" in - keyword ++ spc () ++ name) + keyword ++ spc () ++ name) let print_struct is_impl extent env mp struc = prlist_with_sep spc (print_body is_impl extent env mp) struc @@ -324,7 +324,7 @@ let print_structure ~mod_ops is_type extent env mp locals struc = nametab_register_module_body ~mod_ops mp struc; let kwd = if is_type then "Sig" else "Struct" in hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++ - brk (1,-2) ++ keyword "End") + brk (1,-2) ++ keyword "End") let rec flatten_app mexpr l = match mexpr with | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l) @@ -339,7 +339,7 @@ let rec print_typ_expr extent env mp locals mty = let fapp = List.hd lapp in let mapp = List.tl lapp in hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++ - prlist_with_sep spc (print_modpath locals) mapp ++ str")") + prlist_with_sep spc (print_modpath locals) mapp ++ str")") | MEwith(me,WithDef(idl,(c, _)))-> let s = String.concat "." (List.map Id.to_string idl) in let body = match extent with @@ -378,7 +378,7 @@ let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ - str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ + str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2) let rec print_expression ~mod_ops x = @@ -399,11 +399,11 @@ let rec printable_body dir = try let open Nametab.GlobDirRef in match Nametab.locate_dir (qualid_of_dirpath dir) with - DirOpenModtype _ -> false - | DirModule _ | DirOpenModule _ -> printable_body dir - | _ -> true + DirOpenModtype _ -> false + | DirModule _ | DirOpenModule _ -> printable_body dir + | _ -> true with - Not_found -> true + Not_found -> true (** Since we might play with nametab above, we should reset to prior state after the printing *) |