diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 59 |
1 files changed, 31 insertions, 28 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 8469490f0..a16a92d0a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -51,7 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t = let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env -let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env +let _ = Hook.set Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env = pr_lconstr_core true env let pr_constr_goal_style_env env = pr_constr_core true env @@ -263,16 +263,19 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) = let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) -let pr_var_decl env sigma (id,c,typ) = - pr_var_decl_skel pr_id env sigma (id,c,typ) +let pr_var_decl env sigma d = + pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) let pr_var_list_decl env sigma (l,c,typ) = hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) -let pr_rel_decl env sigma (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> +let pr_rel_decl env sigma decl = + let open Context.Rel.Declaration in + let na = get_name decl in + let typ = get_type decl in + let pbody = match decl with + | LocalAssum _ -> mt () + | LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -294,7 +297,7 @@ let pr_named_context_of env sigma = hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env sigma ne_context = - hv 0 (Context.fold_named_context + hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) ne_context ~init:(mt ())) @@ -307,7 +310,7 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d pps -> let pidt = pr_var_list_decl env sigma d in (pps ++ fnl () ++ pidt)) @@ -334,7 +337,7 @@ let pr_context_limit n env sigma = else let k = lgsign-n in let _,sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d (i,pps) -> if i < k then (i+1, (pps ++str ".")) @@ -417,7 +420,8 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let ids = List.rev_map pi1 l in + let open Context.Named.Declaration in + let ids = List.rev_map get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") @@ -636,8 +640,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s) ++ + (let s = Proof_global.Bullet.suggest p in + if Pp.is_empty s then s else fnl () ++ s) ++ fnl () in pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals @@ -723,7 +727,7 @@ let prterm = pr_lconstr type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant @@ -732,18 +736,17 @@ module OrderedContextObject = struct type t = context_object let compare x y = - match x , y with - | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 - | Axiom _ , Variable _ -> 1 - | Opaque _ , Variable _ - | Opaque _ , Axiom _ -> 1 - | Transparent _ , Variable _ - | Transparent _ , Axiom _ - | Transparent _ , Opaque _ -> 1 - | _ , _ -> -1 + match x , y with + | Variable i1 , Variable i2 -> Id.compare i1 i2 + | Variable _ , _ -> -1 + | _ , Variable _ -> 1 + | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 + | Axiom _ , _ -> -1 + | _ , Axiom _ -> 1 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Opaque _ , _ -> -1 + | _ , Opaque _ -> 1 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 end module ContextObjectSet = Set.Make (OrderedContextObject) @@ -774,7 +777,7 @@ let pr_assumptionset env s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in @@ -783,7 +786,7 @@ let pr_assumptionset env s = let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ str (Names.Label.to_string lbl) ++ + str " used in " ++ pr_label lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) |