aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comInductive.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-03 17:44:34 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-25 14:55:49 +0200
commitdfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch)
tree33fdd7c2eb44e54e7777e2d074127b129c5385ac /vernac/comInductive.ml
parentd2533da244f770261478ae829167cb3a8ad38038 (diff)
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'vernac/comInductive.ml')
-rw-r--r--vernac/comInductive.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 629fcce5a..790e83dbe 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -367,7 +367,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
() in
(* Try further to solve evars, and instantiate them *)
- let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
+ let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
@@ -381,10 +381,10 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
let uctx = Evd.check_univ_decl ~poly sigma decl in
- List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
- Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params;
+ List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+ Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
- List.iter (fun c -> check_evars env_ar_params Evd.empty sigma (EConstr.of_constr c)) ctyps)
+ List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
constructors;
(* Build the inductive entries *)