diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 41 |
1 files changed, 7 insertions, 34 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 77466605a..72030dc9f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -299,8 +299,8 @@ let pr_puniverses f env (c,u) = 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 @@ -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 -> @@ -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 |