diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 01:38:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 17:45:55 +0100 |
| commit | 53f5cc210da4debd5264d6d8651a76281b0b4256 (patch) | |
| tree | 8e1edbb93c15a88480c8bc4454cc9b8fc15c88c1 /vernac/lemmas.ml | |
| parent | c75619228e1c878644edbc49c5cb690777966863 (diff) | |
[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.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 8 |
1 files changed, 3 insertions, 5 deletions
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 |