aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evd.ml4
-rw-r--r--engine/evd.mli4
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/unification.ml4
-rw-r--r--pretyping/unification.mli4
-rw-r--r--tactics/tactics.ml16
-rw-r--r--tactics/tactics.mli2
-rw-r--r--vernac/command.ml8
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/record.ml2
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 02:18:35 +0000