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 /pretyping/recordops.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 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 9eb410f06..56a883099 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -199,7 +199,7 @@ let warn_projection_no_head_constant = let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in + let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") @@ -211,7 +211,7 @@ let compute_canonical_projections warn (con,ind) = let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in let c = Environ.constant_value_in env (con,u) in - let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in let lt = List.rev_map snd sign in @@ -317,7 +317,9 @@ let check_and_decompose_canonical_structure ref = let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref "Could not find its value in the global environment." in - let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in + let env = Global.env () in + let evd = Evd.from_env env in + let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args |