diff options
| author | Gaëtan Gilbert | 2019-10-29 13:20:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:48:53 +0100 |
| commit | 62adf2b9e03afa212fcd8819226da068bf4a32b8 (patch) | |
| tree | f21b6feeec930f418c0a3302fb9c50bfc13c384d /vernac | |
| parent | 1df9e71a1f9b0729a17d09e009add2e87fcde5ad (diff) | |
Pretyping.check_evars: make initial evar map optional
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 6 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 0333b73ffe..c9b5144299 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env = (* Beware of this step, it is required as to minimize universes. *) let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) - Pretyping.check_evars env (Evd.from_env env) sigma termtype; + Pretyping.check_evars env sigma termtype; termtype, sigma let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a001420f74..8a403e5a03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -255,7 +255,7 @@ let context ~poly l = let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in - let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in + let ce t = Pretyping.check_evars env sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in (* reorder, evar-normalize and add implicit status *) let ctx = List.rev_map (fun d -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2aee9bd47f..2afb5e9d65 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -369,10 +369,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; - Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; + List.iter (fun c -> check_evars env_params sigma (EConstr.of_constr (snd c))) arities; + Context.Rel.iter (fun c -> check_evars env0 sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) + List.iter (fun c -> check_evars env_ar_params sigma (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) diff --git a/vernac/record.ml b/vernac/record.ml index d85b71df44..5be911938b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records = in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in let () = List.iter (iter_constr ce) (List.rev newps) in ubinders, univs, template, newps, imps, ans |