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.
---
 engine/evd.ml             |  4 ----
 engine/evd.mli            |  4 ----
 plugins/ltac/tacinterp.ml |  2 +-
 pretyping/pretyping.ml    | 10 +++++-----
 pretyping/pretyping.mli   |  4 ++--
 pretyping/unification.ml  |  4 ++--
 pretyping/unification.mli |  4 ++--
 tactics/tactics.ml        | 16 ++++++----------
 tactics/tactics.mli       |  2 +-
 vernac/command.ml         |  8 ++++----
 vernac/lemmas.ml          |  2 +-
 vernac/record.ml          |  2 +-
 12 files changed, 25 insertions(+), 37 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/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 155cb31d85..6ed96c1fb7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -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/pretyping.ml b/pretyping/pretyping.ml
index f92110ea56..2e215b605d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -333,8 +333,8 @@ let check_evars_are_solved env current_sigma frozen pending =
 
 (* 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,pending = 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
@@ -343,12 +343,12 @@ let solve_remaining_evars flags env current_sigma pending =
   if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
   !evdref
 
-let check_evars_are_solved env current_sigma pending =
-  let frozen,pending = frozen_and_pending_holes pending in
+let check_evars_are_solved env current_sigma init_sigma =
+  let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in
   check_evars_are_solved env current_sigma frozen pending
 
 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/tactics/tactics.ml b/tactics/tactics.ml
index 84d09d8330..1e8082f882 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -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 4b4f4d2711..849596f07b 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 b494430c28..07cfd9ebb7 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 = 
-- 
cgit v1.2.3


From f9526a2bcd05174b7adfe56b7375f0306a2a1e6d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Mar 2017 08:38:00 +0100
Subject: Fast path for implicit tactic solving.

We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
---
 plugins/ltac/extratactics.ml4 |  8 ++++----
 plugins/ltac/g_auto.ml4       |  2 +-
 plugins/ltac/tacinterp.ml     | 22 +++++++++++-----------
 proofs/pfedit.ml              | 12 +++++++++---
 proofs/pfedit.mli             |  2 +-
 tactics/tactics.ml            |  2 +-
 6 files changed, 27 insertions(+), 21 deletions(-)

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 6ed96c1fb7..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
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 1e8082f882..8b3442c05b 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 }
 
-- 
cgit v1.2.3


From 055ff65ac0da60ec76d0f382dab316c3a3302a06 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Mar 2017 09:53:04 +0100
Subject: Fast path in computation of frozen evars in Pretyping.

Most of the time, undefined evars are not modified by the considered function,
which leads to the costly recomputation of a trivial partition of evars. We
simply take advantage of physical equality to discriminate when this is
useless and special-case it in the type of frozen evars.
---
 pretyping/pretyping.ml | 53 +++++++++++++++++++++++++++++++++++---------------
 1 file changed, 37 insertions(+), 16 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2e215b605d..88853045fc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -257,16 +257,33 @@ 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
+  (** 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 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
+    FrozenProgress (frozen, pending)
 
 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 (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 +293,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 (_, pending) ->
   evdref := Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
@@ -299,7 +318,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 (_, pending) ->
   Evar.Set.iter
     (fun evk ->
       if not (Evd.is_defined current_sigma evk) then
@@ -326,26 +347,26 @@ 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 init_sigma =
-  let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in
+  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 init_sigma =
-  let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in
-  check_evars_are_solved env current_sigma frozen pending
+  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 in
-- 
cgit v1.2.3


From 0df06c3778951402c994756a6c20b043bbf2d25f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Mar 2017 11:17:49 +0100
Subject: Make the computation of frozen evars lazy in Pretyping.

A lot of tactic calls actually use the open_constr_no_classes_flags option
which does not require checking anything about frozen evars. Computing it
upfront is useless in this case.
---
 pretyping/pretyping.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 88853045fc..9ed2786602 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -263,7 +263,7 @@ type frozen =
       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
+| 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') =
@@ -272,17 +272,20 @@ let frozen_and_pending_holes (sigma, sigma') =
   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
-    FrozenProgress (frozen, pending)
+    (frozen, pending)
+    end in
+    FrozenProgress data
 
 let apply_typeclasses env evdref frozen fail_evar =
   let filter_frozen = match frozen with
   | FrozenId map -> fun evk -> Evar.Map.mem evk map
-  | FrozenProgress (frozen, _) -> fun evk -> Evar.Set.mem evk frozen
+  | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
   in
   evdref := Typeclasses.resolve_typeclasses
      ~filter:(if Flags.is_program_mode () 
@@ -295,7 +298,7 @@ let apply_typeclasses env evdref frozen fail_evar =
 
 let apply_inference_hook hook evdref frozen = match frozen with
 | FrozenId _ -> ()
-| FrozenProgress (_, pending) ->
+| FrozenProgress (lazy (_, pending)) ->
   evdref := Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
@@ -320,7 +323,7 @@ let check_typeclasses_instances_are_solved env current_sigma frozen =
 
 let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 | FrozenId _ -> ()
-| FrozenProgress (_, pending) ->
+| FrozenProgress (lazy (_, pending)) ->
   Evar.Set.iter
     (fun evk ->
       if not (Evd.is_defined current_sigma evk) then
-- 
cgit v1.2.3


From 8131e35caaacf86cd52262329ab1b0aaa1b8c5b3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Mar 2017 11:29:00 +0100
Subject: Better algorithm for Evarconv.max_undefined_with_candidates.

Instead of crawling the whole undefined evar map, we use the fold_right
function to process evars in decreasing order.
---
 pretyping/evarconv.ml | 28 +++++++++++++++-------------
 1 file changed, 15 insertions(+), 13 deletions(-)

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
-- 
cgit v1.2.3