diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 4 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 4 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 3 | ||||
| -rw-r--r-- | proofs/proof.ml | 11 | ||||
| -rw-r--r-- | proofs/refine.ml | 1 | ||||
| -rw-r--r-- | proofs/refine.mli | 3 |
8 files changed, 15 insertions, 15 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 58c0f7db53..e466992721 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -678,7 +678,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in let ty = Retyping.get_type_of env sigma c in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in + let (sigma, j, _trace) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in let (ev, _) = destEvar sigma ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 611671255d..c6a0299cf3 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -72,7 +72,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd in - Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd' + (* After an apply, all the subgoals including those dependent shelved ones are in + the hands of the user and resolution won't be called implicitely on them. *) + Typeclasses.make_unresolvables (fun x -> true) evd' else clenv.evd in let clenv = { clenv with evd = evd' } in diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 59918ab2f9..8297b11585 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -44,10 +44,10 @@ let define_and_solve_constraints evk c env evd = | Success evd -> evd | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.") -let w_refine (evk,evi) (ltac_var,rawc) sigma = +let w_refine (evk,evi) (ltac_var,rawc) env sigma = if Evd.is_defined sigma evk then user_err Pp.(str "Instantiate called on already-defined evar"); - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in let sigma',typed_c = let flags = { Pretyping.use_typeclasses = true; diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 8f3ac7ed25..a618bf1c94 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -17,4 +17,4 @@ open Ltac_pretype type glob_constr_ltac_closure = ltac_var_map * glob_constr val w_refine : Evar.t * evar_info -> - glob_constr_ltac_closure -> evar_map -> evar_map + glob_constr_ltac_closure -> Environ.env -> evar_map -> evar_map diff --git a/proofs/goal.ml b/proofs/goal.ml index 426fba7f63..4759c0860f 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -31,8 +31,9 @@ module V82 = struct (* Old style env primitive *) let env evars gl = + let env = Global.env () in let evi = Evd.find evars gl in - Evd.evar_filtered_env evi + Evd.evar_filtered_env env evi (* Old style hyps primitive *) let hyps evars gl = diff --git a/proofs/proof.ml b/proofs/proof.ml index 2ee006631a..5ab4409f8b 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -386,12 +386,7 @@ let run_tactic env tac pr = let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in - let proofview = - List.fold_left - Proofview.Unsafe.mark_as_unresolvable - proofview - to_shelve - in + let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace),result @@ -439,10 +434,10 @@ module V82 = struct else CList.nth evl (n-1) in - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in let rawc = intern env sigma in let ltac_vars = Glob_ops.empty_lvar in - let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in + let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) env sigma in Proofview.Unsafe.tclEVARS sigma end in let { name; poly } = pr in diff --git a/proofs/refine.ml b/proofs/refine.ml index dd8b52e56c..ea42218aaa 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -94,6 +94,7 @@ let generic_refine ~typecheck f gl = in (* Mark goals *) let sigma = Proofview.Unsafe.mark_as_goals sigma comb in + let sigma = Proofview.Unsafe.mark_unresolvables sigma shelf in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in diff --git a/proofs/refine.mli b/proofs/refine.mli index bdcccae805..269382489d 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -25,7 +25,8 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions raised during the interpretation of [t] are caught and result in - tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. + Shelved evars and goals are all marked as unresolvable for typeclasses. *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> Proofview.Goal.t -> 'a tactic |