From 53f5cc210da4debd5264d6d8651a76281b0b4256 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 13 Dec 2017 01:38:39 +0100 Subject: [econstr] Switch constrintern API to non-imperative style. We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there. --- vernac/lemmas.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'vernac/lemmas.ml') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7bb56240b..27a680b9b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -92,7 +92,7 @@ let find_mutually_recursive_statements sigma thms = let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in let x = (id,(t,impls)) in let whnf_hyp_hds = EConstr.map_rel_context_in_env - (fun env c -> fst (Reductionops.whd_all_stack env Evd.empty c)) + (fun env c -> fst (Reductionops.whd_all_stack env sigma c)) (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> @@ -441,10 +441,8 @@ let start_proof_com ?inference_hook kind thms hook = | Some decl -> Univdecls.interp_univ_decl_opt env0 (snd decl) in let evd, thms = List.fold_left_map (fun evd (sopt,(bl,t)) -> - let _evdref = ref evd in - let impls, ((env, ctx), imps) = interp_context_evars env0 _evdref bl in - let t', imps' = interp_type_evars_impls ~impls env _evdref t in - let evd = !_evdref in + let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in + let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in let evd = solve_remaining_evars flags env evd Evd.empty in -- cgit v1.2.3