diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 17:44:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 14:55:49 +0200 |
| commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
| tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /printing/printmod.ml | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 3c805b327..be8bc1357 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -323,7 +323,6 @@ let print_body is_impl env mp (l,body) = else Univ.Instance.empty in let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -332,17 +331,17 @@ let print_body is_impl env mp (l,body) = | None -> mt () | Some env -> str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env sigma + hov 0 (Printer.pr_ltype_env env (Evd.from_env env) (Vars.subst_instance_constr u cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env sigma + Printer.pr_lconstr_env env (Evd.from_env env) (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx sigma ctx) + Printer.pr_universe_ctx (Evd.from_env env) ctx) | SFBmind mib -> try let env = Option.get env in @@ -387,7 +386,7 @@ let rec print_typ_expr env mp locals mty = 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 + let sigma = Evd.from_env env 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_env env sigma c) |