diff options
| author | Maxime Dénès | 2019-03-01 15:27:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-20 09:33:15 +0100 |
| commit | 27d453641446b3d35aa2211b94f949b57a88ebb2 (patch) | |
| tree | af47b4cb0e3fbb7fde26b6cab3a9b78b99699e94 /vernac/himsg.ml | |
| parent | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (diff) | |
Stop accessing proof env via Pfedit in printers
This should make https://github.com/coq/coq/pull/9129 easier.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ea97e36744..32754478a5 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -138,7 +138,7 @@ let rec pr_explicit_aux env sigma t1 t2 = function in let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in - Ppconstr.pr_lconstr_expr ct1, Ppconstr.pr_lconstr_expr ct2 + Ppconstr.pr_lconstr_expr env sigma ct1, Ppconstr.pr_lconstr_expr env sigma ct2 let explicit_flags = let open Constrextern in @@ -1091,13 +1091,14 @@ let explain_unbound_method env sigma cid { CAst.v = id } = str "Unbound method name " ++ Id.print (id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." -let pr_constr_exprs exprs = +let pr_constr_exprs env sigma exprs = hv 0 (List.fold_right - (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps) + (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps) exprs (mt ())) let explain_mismatched_contexts env c i j = - let pm, pn = with_diffs (pr_rel_context env (Evd.from_env env) j) (pr_constr_exprs i) in + let sigma = Evd.from_env env in + let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++ fnl () ++ brk (1,1) ++ |