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.

12 files changed, 25 insertions, 37 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 62d396395..b7d56a698 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 993ed300b..5619b7af2 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 155cb31d8..6ed96c1fb 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 f92110ea5..2e215b605 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 2c6aa7a21..23957d557 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 a91c30df6..11771f7ba 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 0ad882a9f..c63502eae 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 84d09d833..1e8082f88 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 7acfb6286..354ac50b4 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 4b4f4d271..849596f07 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 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),
diff --git a/vernac/record.ml b/vernac/record.ml
index b494430c2..07cfd9ebb 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 =