From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 3 May 2018 17:44:34 +0200 Subject: Remove some occurrences of Evd.empty We address the easy ones, but they should probably be all removed. --- engine/termops.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 053fcc3db..bd07555a5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -98,7 +98,10 @@ let rec pr_constr c = match kind c with let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c)) let print_constr_env env sigma t = !term_printer env sigma t -let print_constr t = !term_printer (Global.env()) Evd.empty t +let print_constr t = + let env = Global.env () in + let evd = Evd.from_env env in + !term_printer env evd t let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -340,7 +343,7 @@ let pr_evar_constraints sigma pbs = str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ protect (print_constr_env env Evd.empty) t2 + spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2 in prlist_with_sep fnl pr_evconstr pbs @@ -434,27 +437,29 @@ let pr_metaset metas = let pr_var_decl env decl = let open NamedDecl in + let evd = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env Evd.empty c in + let pb = print_constr_env env evd c in (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in + let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in + let evd = Evd.from_env env in let pbody = match decl with | LocalAssum _ -> mt () | LocalDef (_,c,_) -> (* Force evaluation *) let c = EConstr.of_constr c in - let pb = print_constr_env env Evd.empty c in + let pb = print_constr_env env evd c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in + let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) -- cgit v1.2.3