From 8cfe40dbc02156228a529c01190c50d825495013 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 22 Mar 2017 19:06:54 +0100 Subject: Ensuring static invariants about handling of pending evars in Pretyping. All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. --- vernac/lemmas.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/lemmas.ml') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 798a238c7..409676276 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -463,7 +463,7 @@ let start_proof_com ?inference_hook kind thms hook = let t', imps' = interp_type_evars_impls ~impls env evdref t in let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in - evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); + evdref := solve_remaining_evars flags env !evdref Evd.empty; let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), -- cgit v1.2.3