diff options
| author | Maxime Dénès | 2017-11-21 22:24:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-21 22:24:59 +0100 |
| commit | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /printing/printmod.ml | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
| parent | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff) | |
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 0abca01602..13a03e9b48 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -374,9 +374,12 @@ let rec print_typ_expr env mp locals mty = | MEwith(me,WithDef(idl,(c, _)))-> let env' = None in (* TODO: build a proper environment if env <> None *) let s = String.concat "." (List.map Id.to_string idl) in + (* XXX: What should env and sigma be here? *) + let env = Global.env () in + let sigma = Evd.empty in hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc() ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc() - ++ Printer.pr_lconstr c) + ++ Printer.pr_lconstr_env env sigma c) | MEwith(me,WithMod(idl,mp'))-> let s = String.concat "." (List.map Id.to_string idl) in hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++ |