diff options
| author | Hugo Herbelin | 2018-07-30 17:45:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-30 17:45:05 +0200 |
| commit | 1b2decc1bc0db2a58fcc4a4e6e572aed645bab29 (patch) | |
| tree | 5dc97e6b9fed2414a83d4508d72fc98feba2eff5 /printing/printer.ml | |
| parent | dd84c113a154742dff86328ebc758097e9aac8eb (diff) | |
| parent | d7c52a963588fda638b9f79882a55f56fef6297a (diff) | |
Merge PR #8137: Fix 8132. Print the content of body, not its type.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 8 |
1 files changed, 3 insertions, 5 deletions
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) |