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. --- tactics/class_tactics.ml | 2 +- tactics/eqschemes.ml | 10 ++++++---- tactics/hints.ml | 8 ++++++-- tactics/inv.ml | 5 +++-- 4 files changed, 16 insertions(+), 9 deletions(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ea5d4719c..3e08c6d87 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1174,7 +1174,7 @@ let solve_inst env evd filter unique split fail = let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst -let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = +let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 715686ad0..eede13329 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -78,7 +78,7 @@ let build_dependent_inductive ind (mib,mip) = Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt @ Context.Rel.to_extended_list mkRel 0 realargs) -let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na +let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na let name_assumption env = function | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) @@ -109,7 +109,7 @@ let get_coq_eq ctx = let univ_of_eq env eq = let eq = EConstr.of_constr eq in - match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with + match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false) | _ -> assert false @@ -620,7 +620,9 @@ let build_r2l_forward_rew_scheme dep env ind kind = (**********************************************************************) let fix_r2l_forward_rew_scheme (c, ctx') = - let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in + let env = Global.env () in + let sigma = Evd.from_env env in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in let ctx,_ = decompose_prod_assum t in match ctx with @@ -630,7 +632,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) - (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty + (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma (EConstr.of_constr (applist (c, Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' diff --git a/tactics/hints.ml b/tactics/hints.ml index 3ade5314b..786760122 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1263,7 +1263,9 @@ let prepare_hint check (poly,local) env init (sigma,c) = subst := (evar,mkVar id)::!subst; mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in - if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c'; + let env = Global.env () in + let empty_sigma = Evd.from_env env in + if check then Pretyping.check_evars env empty_sigma sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) @@ -1276,7 +1278,9 @@ let interp_hints poly = let sigma = Evd.from_env env in let f poly c = let evd,c = Constrintern.interp_open_constr env sigma c in - prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in + let env = Global.env () in + let sigma = Evd.from_env env in + prepare_hint true (poly,false) env sigma (evd,c) in let fref r = let gr = global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc gr; diff --git a/tactics/inv.ml b/tactics/inv.ml index 412954989..b346ed223 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -292,7 +292,7 @@ let error_too_many_names pats = str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ str ": " ++ pr_enum (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++ str ".") let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with @@ -496,9 +496,10 @@ let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort Evd.empty k ++ + pr_sort sigma k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e -- cgit v1.2.3