From 6c2a5cba55a831e461e806e08c7be968f9343f7e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 12 Jun 2020 01:18:27 +0200 Subject: Make future_goals stack explicit in the evarmap --- engine/evarutil.ml | 2 +- engine/evd.ml | 172 ++++++++++++++++++++++---------------- engine/evd.mli | 39 ++++----- engine/proofview.ml | 20 +++-- engine/proofview.mli | 2 +- proofs/goal.ml | 14 +--- proofs/proof.ml | 18 ++-- proofs/refine.ml | 19 ++--- tactics/class_tactics.ml | 11 +-- test-suite/bugs/closed/bug_4095.v | 13 +-- vernac/classes.ml | 5 +- 11 files changed, 168 insertions(+), 147 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 9d3ae95e7d..7beb7ff738 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -522,7 +522,7 @@ let restrict_evar evd evk filter ?src candidates = let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in (* Mark new evar as future goal, removing previous one, circumventing Proofview.advance but making Proof.run_tactic catch these. *) - let evd = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) evd in + let evd = Evd.remove_future_goal evd evk in (Evd.declare_future_goal evk' evd, evk') let rec check_and_clear_in_constr env evdref err ids global c = diff --git a/engine/evd.ml b/engine/evd.ml index 9de11bdc1e..584b390cff 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -451,8 +451,6 @@ let key id (_, idtoev) = end -type goal_kind = ToShelve - type evar_flags = { obligation_evars : Evar.Set.t; restricted_evars : Evar.t Evar.Map.t; @@ -466,6 +464,19 @@ type side_effects = { seff_roles : side_effect_role Cmap.t; } +type future_goals = { + future_comb : Evar.t list; + future_shelf : Evar.t list; + future_principal : Evar.t option; (** if [Some e], [e] must be + contained in + [future_comb]. The evar + [e] will inherit + properties (now: the + name) of the evar which + will be instantiated with + a term containing [e]. *) +} + type evar_map = { (* Existential variables *) defn_evars : evar_info EvMap.t; @@ -481,17 +492,8 @@ type evar_map = { evar_flags : evar_flags; (** Interactive proofs *) effects : side_effects; - future_goals : Evar.t list; (** list of newly created evars, to be - eventually turned into goals if not solved.*) - principal_future_goal : Evar.t option; (** if [Some e], [e] must be - contained - [future_goals]. The evar - [e] will inherit - properties (now: the - name) of the evar which - will be instantiated with - a term containing [e]. *) - future_goals_status : goal_kind EvMap.t; + future_goals : future_goals list; (** list of newly created evars, to be + eventually turned into goals if not solved.*) given_up : Evar.Set.t; extras : Store.t; } @@ -591,14 +593,19 @@ let new_evar evd ?name ?typeclass_candidate evi = let remove d e = let undf_evars = EvMap.remove e d.undf_evars in let defn_evars = EvMap.remove e d.defn_evars in - let principal_future_goal = match d.principal_future_goal with - | None -> None - | Some e' -> if Evar.equal e e' then None else d.principal_future_goal + let remove_future fgl = + let future_principal = match fgl.future_principal with + | None -> None + | Some e' -> if Evar.equal e e' then None else fgl.future_principal + in + let filter e' = not (Evar.equal e e') in + let future_comb = List.filter filter fgl.future_comb in + let future_shelf = List.filter filter fgl.future_shelf in + { future_principal; future_comb; future_shelf } in - let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in - let future_goals_status = EvMap.remove e d.future_goals_status in + let future_goals = List.map remove_future d.future_goals in let evar_flags = remove_evar_flags e d.evar_flags in - { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status; + { d with undf_evars; defn_evars; future_goals; evar_flags } let find d e = @@ -714,6 +721,12 @@ let empty_side_effects = { seff_roles = Cmap.empty; } +let empty_future_goals = { + future_principal = None; + future_comb = []; + future_shelf = []; +} + let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; @@ -724,9 +737,7 @@ let empty = { metas = Metamap.empty; effects = empty_side_effects; evar_names = EvNames.empty; (* id<->key for undefined evars *) - future_goals = []; - principal_future_goal = None; - future_goals_status = EvMap.empty; + future_goals = [empty_future_goals]; given_up = Evar.Set.empty; extras = Store.empty; } @@ -1063,73 +1074,94 @@ let drop_side_effects evd = let eval_side_effects evd = evd.effects (* Future goals *) -let declare_future_goal ?tag evk evd = - { evd with future_goals = evk::evd.future_goals; - future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status } - -let declare_principal_goal ?tag evk evd = - match evd.principal_future_goal with - | None -> { evd with - future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; - future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status; +let set_future_goals f = function + | [] -> anomaly Pp.(str"future_goals stack should not be empty") + | hd :: tl -> + f hd :: tl + +let declare_future_goal ?(shelve=false) evk evd = + let add_goal fgl = + let (future_comb,future_shelf) = + if shelve then (fgl.future_comb,evk::fgl.future_shelf) + else (evk::fgl.future_comb,fgl.future_shelf) + in + { fgl with future_comb; future_shelf } + in + let future_goals = set_future_goals add_goal evd.future_goals in + { evd with future_goals } + +let declare_principal_goal ?(shelve=false) evk evd = + let add_goal fgl = + let (future_comb,future_shelf) = + if shelve then (fgl.future_comb,evk::fgl.future_shelf) + else (evk::fgl.future_comb,fgl.future_shelf) + in + let future_principal = Some evk in + { future_comb; future_shelf; future_principal } + in + match (List.hd evd.future_goals).future_principal with + | None -> + let future_goals = set_future_goals add_goal evd.future_goals in + { evd with + future_goals; } | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") -type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t +let push_future_goals evd = + { evd with future_goals = empty_future_goals :: evd.future_goals } -let future_goals evd = evd.future_goals +let pop_future_goals evd = + match evd.future_goals with + | [] -> anomaly Pp.(str"future_goals stack should not be empty") + | hd :: tl -> + hd, { evd with future_goals = tl } -let principal_future_goal evd = evd.principal_future_goal +let future_goals evd = + let future_goals = List.hd evd.future_goals in + future_goals.future_shelf @ future_goals.future_comb -let save_future_goals evd = - (evd.future_goals, evd.principal_future_goal, evd.future_goals_status) - -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal = None; - future_goals_status = EvMap.empty } - -let restore_future_goals evd (gls,pgl,map) = - { evd with future_goals = gls ; principal_future_goal = pgl; - future_goals_status = map } +let principal_future_goal evd = + (List.hd evd.future_goals).future_principal let fold_future_goals f sigma = - List.fold_left f sigma sigma.future_goals + let future_goals = List.hd sigma.future_goals in + let future_goals = future_goals.future_comb @ future_goals.future_shelf in + List.fold_left f sigma future_goals -let map_filter_future_goals f evd = +let map_filter_future_goals f future_goals = (* Note: map is now a superset of filtered evs, but its size should not be too big, so that's probably ok not to update it *) - let future_goals = List.map_filter f evd.future_goals in - let principal_future_goal = Option.bind evd.principal_future_goal f in - { evd with future_goals; principal_future_goal } + let future_comb = List.map_filter f future_goals.future_comb in + let future_shelf = List.map_filter f future_goals.future_shelf in + let future_principal = Option.bind future_goals.future_principal f in + { future_comb; future_shelf; future_principal } -let filter_future_goals f evd = - let future_goals = List.filter f evd.future_goals in - let principal_future_goal = Option.bind evd.principal_future_goal (fun a -> if f a then Some a else None) in - { evd with future_goals; principal_future_goal } +let filter_future_goals f future_goals = + let future_comb = List.filter f future_goals.future_comb in + let future_shelf = List.filter f future_goals.future_shelf in + let future_principal = Option.bind future_goals.future_principal (fun a -> if f a then Some a else None) in + { future_comb; future_shelf; future_principal } let dispatch_future_goals_gen distinguish_shelf evd = - let rec aux (comb,shelf as acc) = function - | [] -> acc - | evk :: gls -> - let acc = - try match EvMap.find evk evd.future_goals_status with - | ToShelve -> - if distinguish_shelf then (comb,evk::shelf) - else raise Not_found - with Not_found -> (evk::comb,shelf) in - aux acc gls in + let future_goals = List.hd evd.future_goals in (* Note: this reverses the order of initial list on purpose *) - let (comb,shelf) = aux ([],[]) evd.future_goals in - (comb,shelf,evd.principal_future_goal) + (List.rev future_goals.future_comb, + List.rev future_goals.future_shelf, + future_goals.future_principal) let dispatch_future_goals = dispatch_future_goals_gen true let shelve_on_future_goals shelved evd = - let future_goals = shelved @ evd.future_goals in - let future_goals_status = List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved evd.future_goals_status in - {evd with future_goals; future_goals_status } + let shelve_future future_goals = + let future_shelf = shelved @ future_goals.future_shelf in + { future_goals with future_shelf } + in + { evd with future_goals = set_future_goals shelve_future evd.future_goals } + +let remove_future_goal evd evk = + let f evk' = not (Evar.equal evk evk') in + { evd with future_goals = set_future_goals (filter_future_goals f) evd.future_goals } let give_up ev evd = { evd with given_up = Evar.Set.add ev evd.given_up } @@ -1152,8 +1184,6 @@ let set_metas evd metas = { effects = evd.effects; evar_names = evd.evar_names; future_goals = evd.future_goals; - future_goals_status = evd.future_goals_status; - principal_future_goal = evd.principal_future_goal; given_up = evd.given_up; extras = evd.extras; } diff --git a/engine/evd.mli b/engine/evd.mli index 4e3f95fc42..7a139e44ba 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -347,13 +347,11 @@ val drop_side_effects : evar_map -> evar_map (** {5 Future goals} *) -type goal_kind = ToShelve - -val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map +val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals. For internal uses only. *) -val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map +val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals and make it principal. Only one existential variable can be made principal, an error is raised otherwise. For internal uses only. *) @@ -366,29 +364,30 @@ val principal_future_goal : evar_map -> Evar.t option (** Retrieves the name of the principal existential variable if there is one. Used by the [refine] primitive of the tactic engine. *) -type future_goals - -val save_future_goals : evar_map -> future_goals -(** Retrieves the list of future goals including the principal future - goal. Used by the [refine] primitive of the tactic engine. *) +type future_goals = { + future_comb : Evar.t list; + future_shelf : Evar.t list; + future_principal : Evar.t option; (** if [Some e], [e] must be + contained in + [future_comb]. The evar + [e] will inherit + properties (now: the + name) of the evar which + will be instantiated with + a term containing [e]. *) +} -val reset_future_goals : evar_map -> evar_map -(** Clears the list of future goals (as well as the principal future - goal). Used by the [refine] primitive of the tactic engine. *) +val push_future_goals : evar_map -> evar_map -val restore_future_goals : evar_map -> future_goals -> evar_map -(** Sets the future goals (including the principal future goal) to a - previous value. Intended to be used after a local list of future - goals has been consumed. Used by the [refine] primitive of the - tactic engine. *) +val pop_future_goals : evar_map -> future_goals * evar_map val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map (** Fold future goals *) -val map_filter_future_goals : (Evar.t -> Evar.t option) -> evar_map -> evar_map +val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals (** Applies a function on the future goals *) -val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map +val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals (** Applies a filter on the future goals *) val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t option @@ -398,6 +397,8 @@ val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t optio val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map (** Push goals on the shelve of future goals *) +val remove_future_goal : evar_map -> Evar.t -> evar_map + val give_up : Evar.t -> evar_map -> evar_map val given_up : evar_map -> Evar.Set.t diff --git a/engine/proofview.ml b/engine/proofview.ml index 0ed945f5d4..21cb6f42a7 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -60,6 +60,10 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) +let map_telescope_evd f = function + | TNil sigma -> TNil (f sigma) + | TCons (env,sigma,ty,g) -> TCons(env,(f sigma),ty,g) + let dependent_init = (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in @@ -74,9 +78,10 @@ let dependent_init = entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } in fun t -> + let t = map_telescope_evd Evd.push_future_goals t in let entry, v = aux t in (* The created goal are not to be shelved. *) - let solution = Evd.reset_future_goals v.solution in + let _goals, solution = Evd.pop_future_goals v.solution in entry, { v with solution } let init = @@ -746,17 +751,16 @@ let with_shelf tac = let open Proof in Pv.get >>= fun pv -> let { shelf; solution } = pv in - Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> + Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >> tac >>= fun ans -> Pv.get >>= fun npv -> let { shelf = gls; solution = sigma } = npv in (* The pending future goals are necessarily coming from V82.tactic *) (* and thus considered as to shelve, as in Proof.run_tactic *) - let gls' = Evd.future_goals sigma in - let fgoals = Evd.save_future_goals solution in - let sigma = Evd.restore_future_goals sigma fgoals in + let fgl, sigma = Evd.pop_future_goals sigma in (* Ensure we mark and return only unsolved goals *) - let gls' = undefined_evars sigma (CList.rev_append gls' gls) in + let gls' = CList.rev_append fgl.Evd.future_shelf (CList.rev_append fgl.Evd.future_comb gls) in + let gls' = undefined_evars sigma gls' in let sigma = mark_in_evm ~goal:false sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -1017,8 +1021,8 @@ module Unsafe = struct let tclEVARUNIVCONTEXT ctx = Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) - let reset_future_goals p = - { p with solution = Evd.reset_future_goals p.solution } + let push_future_goals p = + { p with solution = Evd.push_future_goals p.solution } let mark_as_goals evd content = mark_in_evm ~goal:true evd content diff --git a/engine/proofview.mli b/engine/proofview.mli index 29425b10f2..8853013a84 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -474,7 +474,7 @@ module Unsafe : sig val tclEVARUNIVCONTEXT : UState.t -> unit tactic (** Clears the future goals store in the proof view. *) - val reset_future_goals : proofview -> proofview + val push_future_goals : proofview -> proofview (** Give the evars the status of a goal (changes their source location and makes them unresolvable for type classes. *) diff --git a/proofs/goal.ml b/proofs/goal.ml index 7aea07d6f0..e8f2ab5674 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -56,18 +56,12 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) + let evars = Evd.push_future_goals evars in let inst = EConstr.identity_subst_val hyps in - let evi = { Evd.evar_hyps = hyps; - Evd.evar_concl = concl; - Evd.evar_filter = Evd.Filter.identity; - Evd.evar_abstract_arguments = Evd.Abstraction.identity; - Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); - Evd.evar_candidates = None; - Evd.evar_identity = Evd.Identity.make inst; - } + let (evars,evk) = + Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl in - let (evars, evk) = Evd.new_evar evars ~typeclass_candidate:false evi in + let _, evars = Evd.pop_future_goals evars in let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) diff --git a/proofs/proof.ml b/proofs/proof.ml index 23998f8ba1..11a8023ab6 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -363,28 +363,28 @@ let update_sigma_env p env = let run_tactic env tac pr = let open Proofview.Notations in - let sp = pr.proofview in let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in let tac = tac >>= fun result -> Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in - let retrieved = List.rev @@ Evd.future_goals retrieved in + let retrieved, sigma = Evd.pop_future_goals sigma in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) retrieved in + let retrieved = List.rev_append retrieved.Evd.future_shelf (List.rev retrieved.Evd.future_comb) in let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT (result,retrieved) in - let { name; poly } = pr in + let { name; poly; proofview } = pr in + let proofview = Proofview.Unsafe.push_future_goals proofview in let ((result,retrieved),proofview,(status,to_shelve),info_trace) = - Proofview.apply ~name ~poly env tac sp + Proofview.apply ~name ~poly env tac proofview in 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 = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in - let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf },(status,info_trace),result (*** Commands ***) @@ -569,7 +569,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in (* Save the existing goals *) - let prev_future_goals = Evd.save_future_goals sigma in + let sigma = Evd.push_future_goals sigma in (* Start a proof *) let prf = start ~name ~poly sigma [env, ty] in let (prf, _, ()) = @@ -593,12 +593,12 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in (* Restore former goals *) - let sigma = Evd.restore_future_goals sigma prev_future_goals in + let _goals, sigma = Evd.pop_future_goals sigma in (* Push remaining goals as future_goals which is the only way we have to inform the caller that there are goals to collect while not being encapsulated in the monad *) (* Goals produced by tactic "shelve" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in + let sigma = List.fold_right (Evd.declare_future_goal ~shelve:true) shelf sigma in (* Other goals *) let sigma = List.fold_right Evd.declare_future_goal goals sigma in (* Get rid of the fresh side-effects by internalizing them in the term diff --git a/proofs/refine.ml b/proofs/refine.ml index 4244a9c900..7f0fa587cd 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -51,9 +51,9 @@ let generic_refine ~typecheck f gl = let state = Proofview.Goal.state gl in (* Save the [future_goals] state to restore them after the refinement. *) - let prev_future_goals = Evd.save_future_goals sigma in + let sigma = Evd.push_future_goals sigma in (* Create the refinement term *) - Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> + Proofview.Unsafe.tclEVARS sigma >>= fun () -> f >>= fun (v, c) -> Proofview.tclEVARMAP >>= fun sigma' -> Proofview.V82.wrap_exceptions begin fun () -> @@ -72,17 +72,16 @@ let generic_refine ~typecheck f gl = else Pretype_errors.error_occur_check env sigma self c in (* Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals in + let future_goals, sigma = Evd.pop_future_goals sigma in (* Select the goals *) - let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) sigma' in - let comb,shelf,evkmain = Evd.dispatch_future_goals evs in + let future_goals = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) future_goals in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> (* Nothing to do, the goal has been solved by side-effect *) sigma | Some self -> - match evkmain with + match future_goals.Evd.future_principal with | None -> Evd.define self c sigma | Some evk -> let id = Evd.evar_ident self sigma in @@ -92,16 +91,16 @@ let generic_refine ~typecheck f gl = | Some id -> Evd.rename evk id sigma 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 sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.future_comb in + let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.future_shelf in + let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.future_comb in let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> - Proofview.Unsafe.tclPUTSHELF shelf <*> + Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.future_shelf <*> Proofview.tclUNIT v end diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 597e60093b..ccb69cf845 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -715,8 +715,8 @@ module Search = struct shelve_goals shelved <*> (if List.is_empty goals then tclUNIT () else - let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in - with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>= + let make_unresolvables = tclEVARMAP >>= fun sigma -> Unsafe.tclEVARS @@ make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in + with_shelf (make_unresolvables <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>= fun s -> result s i (Some (Option.default 0 k + j))) end in with_shelf res >>= fun (sh, ()) -> @@ -934,6 +934,7 @@ module Search = struct let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>= fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in let evm = Evd.set_typeclass_evars evm Evar.Set.empty in + let evm = Evd.push_future_goals evm in let _, pv = Proofview.init evm [] in let pv = Proofview.unshelve goalsl pv in try @@ -955,14 +956,14 @@ module Search = struct (str "leaking evar " ++ int (Evar.repr ev) ++ spc () ++ pr_ev evm' ev); acc && okev) evm' true); - let evm = Evd.shelve_on_future_goals shelved evm in - let fgoals = Evd.save_future_goals evm in - let evm' = Evd.restore_future_goals evm' fgoals in + let _, evm' = Evd.pop_future_goals evm' in + let evm' = Evd.shelve_on_future_goals shelved evm' in let nongoals' = Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with | Some ev' -> Evar.Set.add ev acc | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm') in + (* let evm' = { evm' with metas = evm.metas } *) let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in let evm' = Evd.set_typeclass_evars evm' nongoals' in Some evm' diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v index 3d3015c383..d667022e68 100644 --- a/test-suite/bugs/closed/bug_4095.v +++ b/test-suite/bugs/closed/bug_4095.v @@ -71,18 +71,9 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end. Undo. - Fail lazymatch goal with + lazymatch goal with | |- ?R (?f ?a ?b) (?f ?a' ?b') => let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in set(p:=P) - end. (* Toplevel input, characters 15-182: -Error: Cannot infer an instance of type -"PointedOPred" for the variable p in environment: -T : Type -O0 : T -> OPred -O1 : T -> PointedOPred -tr : T -> T -O2 : PointedOPred -x0 : T -H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *) + end. Abort. diff --git a/vernac/classes.ml b/vernac/classes.ml index f454c389dc..5423504f71 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -358,8 +358,9 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code the refinement manually.*) - let gls = List.rev (Evd.future_goals sigma) in - let sigma = Evd.reset_future_goals sigma in + let future_goals, sigma = Evd.pop_future_goals sigma in + let gls = List.rev_append future_goals.Evd.future_shelf (List.rev future_goals.Evd.future_comb) in + let sigma = Evd.push_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Declare.Info.make ~hook ~kind ~udecl ~poly () in -- cgit v1.2.3