diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 63 |
1 files changed, 18 insertions, 45 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 199aa79c6..72030dc9f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -93,13 +93,13 @@ let _ = Hook.set Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c) let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c) -let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c -let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c - let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c let pr_econstr_env env sigma c = pr_econstr_core false env sigma c +let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c +let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c + (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = let (sigma, env) = Pfedit.get_current_context () in @@ -108,12 +108,12 @@ let pr_constr t = let (sigma, env) = Pfedit.get_current_context () in pr_constr_env env sigma t -let pr_open_lconstr (_,c) = pr_lconstr c -let pr_open_constr (_,c) = pr_constr c - let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) +let pr_open_lconstr (_,c) = pr_leconstr c +let pr_open_constr (_,c) = pr_econstr c + let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) @@ -293,14 +293,14 @@ let pr_global = pr_global_env Id.Set.empty let pr_puniverses f env (c,u) = f env c ++ (if !Constrextern.print_universes then - str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" + str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" else mt ()) let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) let pr_existential_key = Termops.pr_existential_key let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev) -let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind) -let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr) +let pr_inductive env ind = pr_lconstr_env env (Evd.from_env env) (mkInd ind) +let pr_constructor env cstr = pr_lconstr_env env (Evd.from_env env) (mkConstruct cstr) let pr_pconstant = pr_puniverses pr_constant let pr_pinductive = pr_puniverses pr_inductive @@ -494,7 +494,7 @@ let pr_transparent_state (ids, csts) = str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) (* display complete goal *) -let default_pr_goal gs = +let pr_goal gs = let g = sig_it gs in let sigma = project gs in let env = Goal.V82.env sigma g in @@ -541,12 +541,12 @@ let pr_evgl_sign sigma evi = if List.is_empty ids then mt () else (str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in - let pc = pr_lconstr_env env sigma evi.evar_concl in + let pc = pr_leconstr_env env sigma evi.evar_concl in let candidates = match evi.evar_body, evi.evar_candidates with | Evar_empty, Some l -> spc () ++ str "= {" ++ - prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}" + prlist_with_sep (fun () -> str "|") (pr_leconstr_env env sigma) l ++ str "}" | _ -> mt () in @@ -591,11 +591,11 @@ let pr_ne_evar_set hd tl sigma l = mt () let pr_selected_subgoal name sigma g = - let pg = default_pr_goal { sigma=sigma ; it=g; } in + let pg = pr_goal { sigma=sigma ; it=g; } in let header = pr_goal_header name sigma g in v 0 (header ++ str " is:" ++ cut () ++ pg) -let default_pr_subgoal n sigma = +let pr_subgoal n sigma = let rec prrec p = function | [] -> user_err Pp.(str "No such goal.") | g::rest -> @@ -622,8 +622,8 @@ let print_evar_constraints gl sigma = end in let pr_evconstr (pbty,env,t1,t2) = - let t1 = Evarutil.nf_evar sigma (EConstr.of_constr t1) - and t2 = Evarutil.nf_evar sigma (EConstr.of_constr t2) in + let t1 = Evarutil.nf_evar sigma t1 + and t2 = Evarutil.nf_evar sigma t2 in let env = (** We currently allow evar instances to refer to anonymous de Bruijn indices, so we protect the error printing code in this case by giving @@ -695,7 +695,7 @@ let print_dependent_evars gl sigma seeds = (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -let default_pr_subgoals ?(pr_first=true) +let pr_subgoals ?(pr_first=true) close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function @@ -739,7 +739,7 @@ let default_pr_subgoals ?(pr_first=true) in let print_multiple_goals g l = if pr_first then - default_pr_goal { it = g ; sigma = sigma; } + pr_goal { it = g ; sigma = sigma; } ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l else @@ -780,33 +780,6 @@ let default_pr_subgoals ?(pr_first=true) ++ print_dependent_evars (Some g1) sigma seeds ) -(**********************************************************************) -(* Abstraction layer *) - - -type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; - pr_subgoal : int -> evar_map -> goal list -> Pp.t; - pr_goal : goal sigma -> Pp.t; -} - -let default_printer_pr = { - pr_subgoals = default_pr_subgoals; - pr_subgoal = default_pr_subgoal; - pr_goal = default_pr_goal; -} - -let printer_pr = ref default_printer_pr - -let set_printer_pr = (:=) printer_pr - -let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x -let pr_subgoal x = !printer_pr.pr_subgoal x -let pr_goal x = !printer_pr.pr_goal x - -(* End abstraction layer *) -(**********************************************************************) - let pr_open_subgoals ~proof = (* spiwack: it shouldn't be the job of the printer to look up stuff in the [evar_map], I did stuff that way because it was more |