diff options
| author | Emilio Jesus Gallego Arias | 2019-12-07 13:45:43 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-07 13:45:43 +0100 |
| commit | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (patch) | |
| tree | c6564c232e5067c2acb48e8c7a4d7ee3ab6ff01a /printing/proof_diffs.ml | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
| parent | f87ce66b88b74f090c316c8a3c33828a970b2108 (diff) | |
Merge PR #11141: Moving the diversity of constr printers to a label style
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 233163d097..dec87f8071 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -245,18 +245,18 @@ let process_goal sigma g : EConstr.t reified_goal = let hyps = List.map to_tuple hyps in { name; ty; hyps; env; sigma };; -let pr_letype_core goal_concl_style env sigma t = - Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_type goal_concl_style env sigma t) +let pr_letype_env ?lax ?goal_concl_style env sigma t = + Ppconstr.pr_lconstr_expr env sigma + (Constrextern.extern_type ?lax ?goal_concl_style env sigma t) let pp_of_type env sigma ty = - pr_letype_core true env sigma ty + pr_letype_env ~goal_concl_style:true env sigma ty -let pr_leconstr_core goal_concl_style env sigma t = - Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr goal_concl_style env sigma t) +let pr_leconstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) -let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) - -let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c +let pr_lconstr_env ?lax ?inctx ?scope env sigma c = + pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) let diff_concl ?og_s nsigma ng = let open Evd in @@ -301,7 +301,7 @@ let goal_info goal sigma = line_idents := idents :: !line_idents; let mid = match body with | Some c -> - let pb = pr_lconstr_env_econstr env sigma c in + let pb = pr_leconstr_env env sigma c in let pb = if EConstr.isCast sigma c then surround pb else pb in str " := " ++ pb | None -> mt() in @@ -556,7 +556,7 @@ let to_constr pf = (* pprf generally has only one element, but it may have more in the derive plugin *) let t = List.hd pprf in let sigma, env = get_proof_context pf in - let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *) + let x = Constrextern.extern_constr env sigma t in (* todo: right options?? *) x.v |