Merge PR#508: Optimize pending evars

17 files changed, 105 insertions, 85 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 62d3963954..b7d56a698e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1157,10 +1157,6 @@ let set_extra_data extras evd = { evd with extras }
 
 (*******************************************************************)
 
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
 type open_constr = evar_map * constr
 
 (*******************************************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index 993ed300bc..5619b7af29 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -601,10 +601,6 @@ val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)
 
-type pending = (* before: *) evar_map * (* after: *) evar_map
-
-type pending_constr = pending * constr
-
 type open_constr = evar_map * constr (* Special case when before is empty *)
 
 (** Partially constructed constrs. *)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1223f6eb4b..7a9fc6657e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
@@ -341,10 +341,10 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-let constr_flags = {
+let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true }
 
@@ -353,7 +353,7 @@ let refine_tac ist simple with_classes c =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags =
-      { constr_flags with Pretyping.use_typeclasses = with_classes } in
+      { constr_flags () with Pretyping.use_typeclasses = with_classes } in
     let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index fcc2b86a91..f75ea70872 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -45,7 +45,7 @@ let eval_uconstrs ist cs =
   let flags = {
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
-    use_hook = Some Pfedit.solve_by_implicit_tactic;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
     fail_evar = false;
     expand_evars = true
   } in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 155cb31d85..fe10f0c313 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   Proofview.NonLogical.run (db_constr (curr_debug ist) env c);
   (evd,c)
 
-let constr_flags = {
+let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = true;
   expand_evars = true }
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  interp_gen kind ist false constr_flags env sigma c
+  interp_gen kind ist false (constr_flags ()) env sigma c
 
 let interp_constr = interp_constr_gen WithoutTypeConstraint
 
 let interp_type = interp_constr_gen IsType
 
-let open_constr_use_classes_flags = {
+let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
-let open_constr_no_classes_flags = {
+let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
-  use_hook = Some solve_by_implicit_tactic;
+  use_hook = solve_by_implicit_tactic ();
   fail_evar = false;
   expand_evars = true }
 
@@ -679,11 +679,11 @@ let pure_open_constr_flags = {
   expand_evars = false }
 
 (* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
   let flags =
-    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
-    else open_constr_use_classes_flags in
-  interp_gen expected_type ist false flags
+    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
+    else open_constr_use_classes_flags () in
+  interp_gen expected_type ist false flags env sigma c
 
 let interp_pure_open_constr ist =
   interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
@@ -1787,7 +1787,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
             (TacLetTac(na,c,clp,b,eqpat))
 	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
                (let_pat_tac b (interp_name ist env sigma na)
-                  ((sigma,sigma'),c) clp eqpat) sigma')
+                  (sigma,c) clp eqpat) sigma')
       end }
 
   (* Derived basic tactics *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 88ea08c840..d18b437a33 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1196,20 +1196,22 @@ let check_problems_are_solved env evd =
   | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
   | _ -> ()
 
+exception MaxUndefined of (Evar.t * evar_info * constr list)
+
 let max_undefined_with_candidates evd =
-  (* If evar were ordered with highest index first, fold_undefined
-     would be going decreasingly and we could use fold_undefined to
-     find the undefined evar of maximum index (alternatively,
-     max_bindings from ocaml 3.12 could be used); instead we traverse
-     the whole map *)
-  let l = Evd.fold_undefined
-    (fun evk ev_info evars ->
-        match ev_info.evar_candidates with
-        | None -> evars
-        | Some l -> (evk,ev_info,l)::evars) evd [] in
-  match l with
-  | [] -> None
-  | a::l -> Some (List.last (a::l))
+  let fold evk evi () = match evi.evar_candidates with
+  | None -> ()
+  | Some l -> raise (MaxUndefined (evk, evi, l))
+  in
+  (** [fold_right] traverses the undefined map in decreasing order of indices.
+  The evar with candidates of maximum index is thus the first evar with
+  candidates found by a [fold_right] traversal. This has a significant impact on
+  performance. *)
+  try
+    let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in
+    None
+  with MaxUndefined ans ->
+    Some ans
 
 let rec solve_unconstrained_evars_with_candidates ts evd =
   (* max_undefined is supposed to return the most recent, hence
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 15a48a6a31..27144b279f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -257,16 +257,36 @@ type inference_flags = {
    [sigma'] into those already in [sigma] or deriving from an evar in
    [sigma] by restriction, and the evars properly created in [sigma'] *)
 
+type frozen =
+| FrozenId of evar_info Evar.Map.t
+  (** No pending evars. We do not put a set here not to reallocate like crazy,
+      but the actual data of the map is not used, only keys matter. All
+      functions operating on this type must have the same behaviour on
+      [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *)
+| FrozenProgress of (Evar.Set.t * Evar.Set.t) Lazy.t
+  (** Proper partition of the evar map as described above. *)
+
 let frozen_and_pending_holes (sigma, sigma') =
-  let add_derivative_of evk evi acc =
-    match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
-  let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
-  let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
-  let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
-  (frozen,pending)
+  let undefined0 = Evd.undefined_map sigma in
+  (** Fast path when the undefined evars where not modified *)
+  if undefined0 == Evd.undefined_map sigma' then
+    FrozenId undefined0
+  else
+    let data = lazy begin
+    let add_derivative_of evk evi acc =
+      match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+    let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in
+    let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+    let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+    (frozen, pending)
+    end in
+    FrozenProgress data
 
 let apply_typeclasses env evdref frozen fail_evar =
-  let filter_frozen evk = Evar.Set.mem evk frozen in
+  let filter_frozen = match frozen with
+  | FrozenId map -> fun evk -> Evar.Map.mem evk map
+  | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
+  in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
 	      then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -276,7 +296,9 @@ let apply_typeclasses env evdref frozen fail_evar =
     evdref := Typeclasses.resolve_typeclasses
       ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref
 
-let apply_inference_hook hook evdref pending =
+let apply_inference_hook hook evdref frozen = match frozen with
+| FrozenId _ -> ()
+| FrozenProgress (lazy (_, pending)) ->
   evdref := Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
@@ -299,7 +321,9 @@ let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
   apply_typeclasses env (ref current_sigma) frozen true
 
-let check_extra_evars_are_solved env current_sigma pending =
+let check_extra_evars_are_solved env current_sigma frozen = match frozen with
+| FrozenId _ -> ()
+| FrozenProgress (lazy (_, pending)) ->
   Evar.Set.iter
     (fun evk ->
       if not (Evd.is_defined current_sigma evk) then
@@ -326,29 +350,29 @@ let check_evars env initial_sigma sigma c =
       | _ -> Constr.iter proc_rec c
   in proc_rec c
 
-let check_evars_are_solved env current_sigma frozen pending =
+let check_evars_are_solved env current_sigma frozen =
   check_typeclasses_instances_are_solved env current_sigma frozen;
   check_problems_are_solved env current_sigma;
-  check_extra_evars_are_solved env current_sigma pending
+  check_extra_evars_are_solved env current_sigma frozen
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
-let solve_remaining_evars flags env current_sigma pending =
-  let frozen,pending = frozen_and_pending_holes pending in
+let solve_remaining_evars flags env current_sigma init_sigma =
+  let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
   let evdref = ref current_sigma in
   if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
   if Option.has_some flags.use_hook then
-    apply_inference_hook (Option.get flags.use_hook env) evdref pending;
+    apply_inference_hook (Option.get flags.use_hook env) evdref frozen;
   if flags.solve_unification_constraints then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
+  if flags.fail_evar then check_evars_are_solved env !evdref frozen;
   !evdref
 
-let check_evars_are_solved env current_sigma pending =
-  let frozen,pending = frozen_and_pending_holes pending in
-  check_evars_are_solved env current_sigma frozen pending
+let check_evars_are_solved env current_sigma init_sigma =
+  let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
+  check_evars_are_solved env current_sigma frozen
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
-  let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in
+  let sigma = solve_remaining_evars flags env sigma initial_sigma in
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2c6aa7a21b..23957d5575 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -129,13 +129,13 @@ val type_uconstr :
    [pending], however, it can contain more evars than the pending ones. *)
 
 val solve_remaining_evars : inference_flags ->
-  env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
+  env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map
 
 (** Checking evars and pending conversion problems are all solved,
     reporting an appropriate error message *)
 
 val check_evars_are_solved :
-  env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
+  env -> (* current map: *) evar_map -> (* initial map: *) evar_map -> unit
 
 (** [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a91c30df6f..11771f7bac 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1520,7 +1520,7 @@ let default_matching_merge_flags sigma =
     use_pattern_unification = true;
 }
 
-let default_matching_flags (sigma,_) =
+let default_matching_flags sigma =
   let flags = default_matching_core_flags sigma in {
   core_unify_flags = flags;
   merge_unify_flags = default_matching_merge_flags sigma;
@@ -1658,7 +1658,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
 type prefix_of_inductive_support_flag = bool
 
 type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * (evar_map * constr) * clause * bool
 | AbstractExact of Name.t * constr * types option * clause * bool
 
 type 'r abstraction_result =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0ad882a9ff..c63502eae1 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -71,11 +71,11 @@ exception PatternNotFound
 type prefix_of_inductive_support_flag = bool
 
 type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool
 | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
 
 val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
-  env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma
+  env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b06ea43bdd..9995a9394a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -233,10 +233,10 @@ let declare_implicit_tactic tac = implicit_tactic := Some tac
 
 let clear_implicit_tactic () = implicit_tactic := None
 
-let solve_by_implicit_tactic env sigma evk =
+let apply_implicit_tactic tac = (); fun env sigma evk ->
   let evi = Evd.find_undefined sigma evk in
-  match (!implicit_tactic, snd (evar_source evk sigma)) with
-  | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
+  match snd (evar_source evk sigma) with
+  | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _)
       when
 	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
@@ -250,3 +250,9 @@ let solve_by_implicit_tactic env sigma evk =
         sigma, ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
+
+let solve_by_implicit_tactic () = match !implicit_tactic with
+| None -> None
+| Some tac -> Some (apply_implicit_tactic tac)
+
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7458109fa1..aad719db49 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
+val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr) option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a78037ce2..0aab773140 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1146,7 +1146,7 @@ let run_delayed env sigma c =
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = Some solve_by_implicit_tactic;
+  Pretyping.use_hook = solve_by_implicit_tactic ();
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
@@ -1154,10 +1154,9 @@ let tactic_infer_flags with_evar = {
 let onOpenInductionArg env sigma tac = function
   | clear_flag,ElimOnConstr f ->
       let (cbl, sigma') = run_delayed env sigma f in
-      let pending = (sigma,sigma') in
       Tacticals.New.tclTHEN
         (Proofview.Unsafe.tclEVARS sigma')
-        (tac clear_flag (pending,cbl))
+        (tac clear_flag (sigma,cbl))
   | clear_flag,ElimOnAnonHyp n ->
       Tacticals.New.tclTHEN
         (intros_until_n n)
@@ -1165,8 +1164,7 @@ let onOpenInductionArg env sigma tac = function
            (fun c ->
              Proofview.Goal.enter { enter = begin fun gl ->
              let sigma = Tacmach.New.project gl in
-             let pending = (sigma,sigma) in
-             tac clear_flag (pending,(c,NoBindings))
+             tac clear_flag (sigma,(c,NoBindings))
              end }))
   | clear_flag,ElimOnIdent (_,id) ->
       (* A quantified hypothesis *)
@@ -1174,8 +1172,7 @@ let onOpenInductionArg env sigma tac = function
         (try_intros_until_id_check id)
         (Proofview.Goal.enter { enter = begin fun gl ->
          let sigma = Tacmach.New.project gl in
-         let pending = (sigma,sigma) in
-         tac clear_flag (pending,(mkVar id,NoBindings))
+         tac clear_flag (sigma,(mkVar id,NoBindings))
         end })
 
 let onInductionArg tac = function
@@ -1198,10 +1195,9 @@ let map_destruction_arg f sigma = function
 
 let finish_delayed_evar_resolution with_evars env sigma f =
   let ((c, lbind), sigma') = run_delayed env sigma f in
-  let pending = (sigma,sigma') in
   let sigma' = Sigma.Unsafe.of_evar_map sigma' in
   let flags = tactic_infer_flags with_evars in
-  let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in
+  let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in
   (Sigma.to_evar_map sigma', (c, lbind))
 
 let with_no_bindings (c, lbind) =
@@ -4525,11 +4521,11 @@ let induction_destruct isrec with_evars (lc,elim) =
 
 let induction ev clr c l e =
   induction_gen clr true ev e 
-    (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None
+    ((Evd.empty,(c,NoBindings)),(None,l)) None
 
 let destruct ev clr c l e =
   induction_gen clr false ev e
-    (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None
+    ((Evd.empty,(c,NoBindings)),(None,l)) None
 
 (* The registered tactic, which calls the default elimination
  * if no elimination constant is provided. *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7acfb62864..354ac50b43 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -385,7 +385,7 @@ val letin_tac : (bool * intro_pattern_naming) option ->
 (** Common entry point for user-level "set", "pose" and "remember" *)
 
 val letin_pat_tac : (bool * intro_pattern_naming) option ->
-  Name.t -> pending_constr -> clause -> unit Proofview.tactic
+  Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic
 
 (** {6 Generalize tactics. } *)
 
diff --git a/vernac/command.ml b/vernac/command.ml
index 8244ee5346..6eb7037f84 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -139,7 +139,7 @@ let interp_definition pl bl p red_option c ctypopt =
   red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
 
 let check_definition (ce, evd, _, imps) =
-  check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
+  check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
 let warn_local_declaration =
@@ -299,7 +299,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
       ((env,ienv),((is_coe,idl),t,imps))) 
     (env,empty_internalization_env) l
   in
-  let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in
+  let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
   (* The universe constraints come from the whole telescope. *)
   let evd = Evd.nf_constraints evd in
   let ctx = Evd.universe_context_set evd in
@@ -604,7 +604,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
      () in
 
   (* Try further to solve evars, and instantiate them *)
-  let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in
+  let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref Evd.empty in
   evdref := sigma;
   (* Compute renewed arities *)
   let nf,_ = e_nf_evars_and_universes evdref in
@@ -1142,7 +1142,7 @@ let interp_recursive isfix fixl notations =
   (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
-  check_evars_are_solved env evd (Evd.empty,evd);
+  check_evars_are_solved env evd Evd.empty;
   if List.for_all Option.has_some fixdefs then begin
     let fixdefs = List.map Option.get fixdefs in
     check_mutuality env isfix (List.combine fixnames fixdefs)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 798a238c74..409676276a 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),
diff --git a/vernac/record.ml b/vernac/record.ml
index 51d89f1551..288d3391bb 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -141,7 +141,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
   in
   let sigma = 
-    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
+    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
   let evars, nf = Evarutil.nf_evars_and_universes sigma in
   let arity = nf t' in
   let arity, evars =