diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 8 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 14 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 6 |
4 files changed, 21 insertions, 9 deletions
@@ -135,7 +135,7 @@ Display diffs between proof steps - coqtop and coqide can now highlight the differences between proof steps in color. This can be enabled from the command line or the - "Set Diffs on|off|removed" command. Please see the documentation for + `Set Diffs "on"|"off"|"removed"` command. Please see the documentation for details. Showing diffs in Proof General requires small changes to PG (under discussion). diff --git a/printing/printer.ml b/printing/printer.ml index a77c1ced56..5b3ead181f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -82,11 +82,10 @@ let pr_econstr_n_core goal_concl_style env sigma n t = pr_constr_expr_n n (extern_constr goal_concl_style env sigma t) let pr_econstr_core goal_concl_style env sigma t = pr_constr_expr (extern_constr goal_concl_style env sigma t) -let pr_leconstr_core goal_concl_style env sigma t = - pr_lconstr_expr (extern_constr goal_concl_style env sigma t) +let pr_leconstr_core = Proof_diffs.pr_leconstr_core let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c) -let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) +let pr_lconstr_env = Proof_diffs.pr_lconstr_env let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) let _ = Hook.set Refine.pr_constr pr_constr_env @@ -133,8 +132,7 @@ let pr_lconstr_under_binders c = let pr_etype_core goal_concl_style env sigma t = pr_constr_expr (extern_type goal_concl_style env sigma t) -let pr_letype_core goal_concl_style env sigma t = - pr_lconstr_expr (extern_type goal_concl_style env sigma t) +let pr_letype_core = Proof_diffs.pr_letype_core let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c) let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 7131ced15b..3a81e908a7 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -251,6 +251,11 @@ let pr_letype_core goal_concl_style env sigma t = let pp_of_type env sigma ty = pr_letype_core true env sigma EConstr.(of_constr ty) +let pr_leconstr_core goal_concl_style env sigma t = + Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t) + +let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) + (* fetch info from a goal, returning (idents, map, concl_pp) where idents is a list with one entry for each hypothesis, each entry is the list of idents on the lhs of the hypothesis. map is a map from ident to hyp_info @@ -278,10 +283,13 @@ let goal_info goal sigma = line_idents := idents :: !line_idents; let mid = match body with - | Some x -> str " := " ++ pp_of_type env sigma ty ++ str " : " - | None -> str " : " in + | Some c -> + let pb = pr_lconstr_env env sigma c in + let pb = if Constr.isCast c then surround pb else pb in + str " := " ++ pb + | None -> mt() in let ts = pp_of_type env sigma ty in - let rhs_pp = mid ++ ts in + let rhs_pp = mid ++ str " : " ++ ts in let make_entry () = { idents; rhs_pp; done_ = false } in List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index 0d3b5821e5..482f03b686 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -30,6 +30,8 @@ val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t open Evd open Proof_type +open Environ +open Constr (** Computes the diff between two goals @@ -46,6 +48,10 @@ val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list +val pr_letype_core : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t +val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t +val pr_lconstr_env : env -> evar_map -> constr -> Pp.t + (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) val log_out_ch : out_channel ref |