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/comInductive.ml | |
| 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/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 *) |