aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh6
-rw-r--r--engine/proofview.ml133
-rw-r--r--engine/proofview.mli15
-rw-r--r--engine/proofview_monad.ml30
-rw-r--r--engine/proofview_monad.mli21
-rw-r--r--plugins/ltac/extratactics.ml41
-rw-r--r--plugins/ltac/rewrite.ml3
-rw-r--r--proofs/refine.ml2
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--vernac/classes.ml2
10 files changed, 153 insertions, 64 deletions
diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
new file mode 100644
index 000000000..2451657d4
--- /dev/null
+++ b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then
+ ltac2_CI_BRANCH=fix-for/6676
+ ltac2_CI_GITURL=https://github.com/gares/ltac2.git
+ Equations_CI_BRANCH=fix-for/6676
+ Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
+fi
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c41b0b0dc..77a884121 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -33,7 +33,7 @@ type entry = (EConstr.constr * EConstr.types) list
(* In this version: returns the list of focused goals together with
the [evar_map] context. *)
let proofview p =
- p.comb , p.solution
+ List.map drop_state p.comb , p.solution
let compact el ({ solution } as pv) =
let nf c = Evarutil.nf_evar solution c in
@@ -74,7 +74,7 @@ let dependent_init =
let (gl, _) = EConstr.destEvar sigma econstr in
let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
let entry = (econstr, typ) :: ret in
- entry, { solution = sol; comb = gl :: comb; shelf = [] }
+ entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
in
fun t ->
let entry, v = aux t in
@@ -110,7 +110,7 @@ let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry)
(* First component is a reverse list of the goals which come before
and second component is the list of the goals which go after (in
the expected order). *)
-type focus_context = Evar.t list * Evar.t list
+type focus_context = goal_with_state list * goal_with_state list
(** Returns a stylised view of a focus_context for use by, for
@@ -120,7 +120,8 @@ type focus_context = Evar.t list * Evar.t list
new nearly identical function everytime. Hence the generic name. *)
(* In this version: the goals in the context, as a "zipper" (the first
list is in reversed order). *)
-let focus_context f = f
+let focus_context (left,right) =
+ (List.map drop_state left, List.map drop_state right)
(** This (internal) function extracts a sublist between two indices,
and returns this sublist together with its context: if it returns
@@ -149,21 +150,35 @@ let unfocus_sublist (left,right) s =
proofview. It returns the focused proofview, and a context for
the focus stack. *)
let focus i j sp =
- let (new_comb, context) = focus_sublist i j sp.comb in
- ( { sp with comb = new_comb } , context )
+ let (new_comb, (left, right)) = focus_sublist i j sp.comb in
+ ( { sp with comb = new_comb } , (left, right) )
+
+let cleared_alias evd g =
+ let evk = drop_state g in
+ let state = get_state g in
+ Option.map (fun g -> goal_with_state g state) (Evarutil.advance evd evk)
(** [undefined defs l] is the list of goals in [l] which are still
unsolved (after advancing cleared goals). Note that order matters. *)
-let undefined defs l =
+let undefined_evars defs l =
List.fold_right (fun evk l ->
match Evarutil.advance defs evk with
| Some evk -> List.add_set Evar.equal evk l
| None -> l) l []
+let goal_with_state_equal x y = Evar.equal (drop_state x) (drop_state y)
+let undefined defs l =
+ List.fold_right (fun evk l ->
+ match cleared_alias defs evk with
+ | Some evk -> List.add_set goal_with_state_equal evk l
+ | None -> l) l []
(** Unfocuses a proofview with respect to a context. *)
-let unfocus c sp =
- { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) }
+let unfocus (left, right) sp =
+ { sp with comb = undefined sp.solution (unfocus_sublist (left, right) sp.comb) }
+let with_empty_state = Proofview_monad.with_empty_state
+let drop_state = Proofview_monad.drop_state
+let goal_with_state = Proofview_monad.goal_with_state
(** {6 The tactic monad} *)
@@ -406,7 +421,8 @@ let tclFOCUSID id t =
try
let ev = Evd.evar_key id initial.solution in
try
- let n = CList.index Evar.equal ev initial.comb in
+ let comb = CList.map drop_state initial.comb in
+ let n = CList.index Evar.equal ev comb in
(* goal is already under focus *)
let (focused,context) = focus n n initial in
Pv.set focused >>
@@ -415,7 +431,7 @@ let tclFOCUSID id t =
return result
with Not_found ->
(* otherwise, save current focus and work purely on the shelve *)
- Comb.set [ev] >>
+ Comb.set [with_empty_state ev] >>
t >>= fun result ->
Comb.set initial.comb >>
return result
@@ -445,7 +461,7 @@ let iter_goal i =
Comb.get >>= fun initial ->
Proof.List.fold_left begin fun (subgoals as cur) goal ->
Solution.get >>= fun step ->
- match Evarutil.advance step goal with
+ match cleared_alias step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
@@ -462,7 +478,7 @@ let map_goal i =
Comb.get >>= fun initial ->
Proof.List.fold_left begin fun (acc, subgoals as cur) goal ->
Solution.get >>= fun step ->
- match Evarutil.advance step goal with
+ match cleared_alias step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
@@ -488,7 +504,7 @@ let fold_left2_goal i s l =
in
Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
Solution.get >>= fun step ->
- match Evarutil.advance step goal with
+ match cleared_alias step goal with
| None -> return cur
| Some goal ->
Comb.set [goal] >>
@@ -532,7 +548,7 @@ let tclDISPATCHGEN0 join tacs =
let open Proof in
Pv.get >>= function
| { comb=[goal] ; solution } ->
- begin match Evarutil.advance solution goal with
+ begin match cleared_alias solution goal with
| None -> tclUNIT (join [])
| Some _ -> Proof.map (fun res -> join [res]) tac
end
@@ -624,12 +640,12 @@ let shelve =
Comb.get >>= fun initial ->
Comb.set [] >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
- Shelf.modify (fun gls -> gls @ initial)
+ Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
let shelve_goals l =
let open Proof in
Comb.get >>= fun initial ->
- let comb = CList.filter (fun g -> not (CList.mem g l)) initial in
+ let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
Comb.set comb >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_goals")) >>
Shelf.modify (fun gls -> gls @ l)
@@ -656,9 +672,27 @@ let free_evars sigma l =
in
List.map map l
+let free_evars_with_state sigma l =
+ let cache = Evarutil.create_undefined_evars_cache () in
+ let map ev =
+ (** Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
+ let ev = drop_state ev in
+ let evi = Evd.find sigma ev in
+ let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
+ (ev, fevs)
+ in
+ List.map map l
+
+
(** [unifiable sigma g l] checks whether [g] appears in another
subgoal of [l]. The list [l] may contain [g], but it does not
affect the result. *)
+let unifiable_delayed_with_state sigma g l =
+ let g = drop_state g in
+ unifiable_delayed g l
+
let unifiable sigma g l =
let l = free_evars sigma l in
unifiable_delayed g l
@@ -668,8 +702,8 @@ let unifiable sigma g l =
whose definition other goals of [l] depend, and [n] are the
non-unifiable goals. *)
let partition_unifiable sigma l =
- let fevs = free_evars sigma l in
- CList.partition (fun g -> unifiable_delayed g fevs) l
+ let fevs = free_evars_with_state sigma l in
+ CList.partition (fun g -> unifiable_delayed_with_state sigma g fevs) l
(** Shelves the unifiable goals under focus, i.e. the goals which
appear in other goals under focus (the unfocused goals are not
@@ -680,7 +714,7 @@ let shelve_unifiable =
let (u,n) = partition_unifiable initial.solution initial.comb in
Comb.set n >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
- Shelf.modify (fun gls -> gls @ u)
+ Shelf.modify (fun gls -> gls @ CList.map drop_state u)
(** [guard_no_unifiable] returns the list of unifiable goals if some
goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
@@ -691,13 +725,14 @@ let guard_no_unifiable =
match u with
| [] -> tclUNIT None
| gls ->
- let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in
+ let l = CList.map (fun g -> Evd.dependent_evar_ident (drop_state g) initial.solution) gls in
let l = CList.map (fun id -> Names.Name id) l in
tclUNIT (Some l)
(** [unshelve l p] adds all the goals in [l] at the end of the focused
goals of p *)
let unshelve l p =
+ let l = List.map with_empty_state l in
(* advance the goals in case of clear *)
let l = undefined p.solution l in
{ p with comb = p.comb@l }
@@ -736,7 +771,7 @@ let with_shelf tac =
let pgoal = Evd.principal_future_goal solution in
let sigma = Evd.restore_future_goals sigma fgoals pgoal in
(* Ensure we mark and return only unsolved goals *)
- let gls' = undefined sigma (CList.rev_append gls' gls) in
+ let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
let npv = { npv with shelf; solution = sigma } in
Pv.set npv >> tclUNIT (gls', ans)
@@ -818,7 +853,7 @@ let give_up =
Comb.set [] >>
mark_as_unsafe >>
InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
- Giveup.put initial
+ Giveup.put (CList.map drop_state initial)
@@ -859,8 +894,8 @@ module Progress = struct
(** Equality function on goals *)
let goal_equal evars1 gl1 evars2 gl2 =
- let evi1 = Evd.find evars1 gl1 in
- let evi2 = Evd.find evars2 gl2 in
+ let evi1 = Evd.find evars1 (drop_state gl1) in
+ let evi2 = Evd.find evars2 (drop_state gl2) in
eq_evar_info evars1 evars2 evi1 evi2
end
@@ -1027,10 +1062,12 @@ module Goal = struct
env : Environ.env;
sigma : Evd.evar_map;
concl : EConstr.constr ;
+ state : StateStore.t;
self : Evar.t ; (* for compatibility with old-style definitions *)
}
let assume (gl : t) = (gl : t)
+ let state { state=state } = state
let env {env} = env
let sigma {sigma} = sigma
@@ -1038,16 +1075,19 @@ module Goal = struct
let concl {concl} = concl
let extra {sigma; self} = goal_extra sigma self
- let gmake_with info env sigma goal =
+ let gmake_with info env sigma goal state =
{ env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
sigma = sigma ;
concl = EConstr.of_constr (Evd.evar_concl info);
+ state = state ;
self = goal }
let nf_gmake env sigma goal =
+ let state = get_state goal in
+ let goal = drop_state goal in
let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in
let sigma = Evd.add sigma goal info in
- gmake_with info env sigma goal , sigma
+ gmake_with info env sigma goal state , sigma
let nf_enter f =
InfoL.tag (Info.Dispatch) begin
@@ -1063,15 +1103,17 @@ module Goal = struct
end
end
- let normalize { self } =
+ let normalize { self; state } =
Env.get >>= fun env ->
tclEVARMAP >>= fun sigma ->
- let (gl,sigma) = nf_gmake env sigma self in
+ let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
let gmake env sigma goal =
+ let state = get_state goal in
+ let goal = drop_state goal in
let info = Evd.find sigma goal in
- gmake_with info env sigma goal
+ gmake_with info env sigma goal state
let enter f =
let f gl = InfoL.tag (Info.DBranch) (f gl) in
@@ -1104,7 +1146,7 @@ module Goal = struct
Pv.get >>= fun step ->
let sigma = step.solution in
let map goal =
- match Evarutil.advance sigma goal with
+ match cleared_alias sigma goal with
| None -> None (** ppedrot: Is this check really necessary? *)
| Some goal ->
let gl =
@@ -1164,18 +1206,22 @@ module V82 = struct
let open Proof in
Pv.get >>= fun ps ->
try
- let tac gl evd =
+ let tac g_w_s evd =
+ let g, w = drop_state g_w_s, get_state g_w_s in
let glsigma =
- tac { Evd.it = gl ; sigma = evd; } in
+ tac { Evd.it = g ; sigma = evd; } in
let sigma = glsigma.Evd.sigma in
- let g = glsigma.Evd.it in
+ let g = CList.map (fun g -> goal_with_state g w) glsigma.Evd.it in
( g, sigma )
in
(* Old style tactics expect the goals normalized with respect to evars. *)
- let (initgoals,initevd) =
- Evd.Monad.List.map (fun g s -> goal_nf_evar s g) ps.comb ps.solution
+ let (initgoals_w_state, initevd) =
+ Evd.Monad.List.map (fun g_w_s s ->
+ let g, w = drop_state g_w_s, get_state g_w_s in
+ let g, s = goal_nf_evar s g in
+ goal_with_state g w, s) ps.comb ps.solution
in
- let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
+ let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in
let sgs = CList.flatten goalss in
let sgs = undefined evd sgs in
InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
@@ -1190,8 +1236,9 @@ module V82 = struct
let nf_evar_goals =
Pv.modify begin fun ps ->
let map g s = goal_nf_evar s g in
- let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
- { ps with solution = evd; comb = goals; }
+ let comb = CList.map drop_state ps.comb in
+ let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in
+ { ps with solution = evd; }
end
let has_unresolved_evar pv =
@@ -1201,14 +1248,14 @@ module V82 = struct
let grab pv =
let undef = Evd.undefined_map pv.solution in
let goals = CList.rev_map fst (Evar.Map.bindings undef) in
- { pv with comb = goals }
+ { pv with comb = List.map with_empty_state goals }
(* Returns the open goals of the proofview together with the evar_map to
interpret them. *)
let goals { comb = comb ; solution = solution; } =
- { Evd.it = comb ; sigma = solution }
+ { Evd.it = List.map drop_state comb ; sigma = solution }
let top_goals initial { solution=solution; } =
let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
@@ -1222,9 +1269,9 @@ module V82 = struct
let of_tactic t gls =
try
- let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+ let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in
- { Evd.sigma = final.solution ; it = final.comb }
+ { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
with Logic_monad.TacticFailure e as src ->
let (_, info) = CErrors.push src in
iraise (e, info)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 721ce507d..77f30746d 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -72,7 +72,15 @@ val return : proofview -> Evd.evar_map
val partial_proof : entry -> proofview -> constr list
val initial_goals : entry -> (constr * types) list
+(** goal <-> goal_with_state *)
+val with_empty_state :
+ Proofview_monad.goal -> Proofview_monad.goal_with_state
+val drop_state :
+ Proofview_monad.goal_with_state -> Proofview_monad.goal
+val goal_with_state :
+ Proofview_monad.goal -> Proofview_monad.StateStore.t ->
+ Proofview_monad.goal_with_state
(** {6 Focusing commands} *)
@@ -416,14 +424,14 @@ module Unsafe : sig
(** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
being proved, appending them to the list of focused goals. If a
goal is already solved, it is not added. *)
- val tclNEWGOALS : Evar.t list -> unit tactic
+ val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic
(** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
goal is already solved, it is not set. *)
- val tclSETGOALS : Evar.t list -> unit tactic
+ val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic
(** [tclGETGOALS] returns the list of goals under focus. *)
- val tclGETGOALS : Evar.t list tactic
+ val tclGETGOALS : Proofview_monad.goal_with_state list tactic
(** Sets the evar universe context. *)
val tclEVARUNIVCONTEXT : UState.t -> unit tactic
@@ -480,6 +488,7 @@ module Goal : sig
val env : t -> Environ.env
val sigma : t -> Evd.evar_map
val extra : t -> Evd.Store.t
+ val state : t -> Proofview_monad.StateStore.t
(** [nf_enter t] applies the goal-dependent tactic [t] in each goal
independently, in the manner of {!tclINDEPENDENT} except that
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index d0f471225..494765fc4 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -149,13 +149,25 @@ module Info = struct
CList.map_append (collapse_tree n) f
end
+module StateStore = Store.Make(struct end)
+
+(* let (set_state, get_state) = StateDyn.Easy.make_dyn "goal_state" *)
+
+type goal = Evar.t
+type goal_with_state = Evar.t * StateStore.t
+
+let drop_state = fst
+let get_state = snd
+let goal_with_state g s = (g, s)
+let with_empty_state g = (g, StateStore.empty)
+let map_goal_with_state f (g, s) = (f g, s)
(** Type of proof views: current [evar_map] together with the list of
focused goals. *)
type proofview = {
solution : Evd.evar_map;
- comb : Evar.t list;
- shelf : Evar.t list;
+ comb : goal_with_state list;
+ shelf : goal list;
}
(** {6 Instantiation of the logic monad} *)
@@ -169,7 +181,7 @@ module P = struct
type e = bool
(** Status (safe/unsafe) * shelved goals * given up *)
- type w = bool * Evar.t list
+ type w = bool * goal list
let wunit = true , []
let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
@@ -209,9 +221,9 @@ module Solution : State with type t := Evd.evar_map = struct
let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution })
end
-module Comb : State with type t = Evar.t list = struct
+module Comb : State with type t = goal_with_state list = struct
(* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
- type t = Evar.t list
+ type t = goal_with_state list
let get = Logical.map (fun {comb} -> comb) Pv.get
let set c = Pv.modify (fun pv -> { pv with comb = c })
let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb })
@@ -227,17 +239,17 @@ module Status : Writer with type t := bool = struct
let put s = Logical.put (s, [])
end
-module Shelf : State with type t = Evar.t list = struct
+module Shelf : State with type t = goal list = struct
(* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
- type t = Evar.t list
+ type t = goal list
let get = Logical.map (fun {shelf} -> shelf) Pv.get
let set c = Pv.modify (fun pv -> { pv with shelf = c })
let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
end
-module Giveup : Writer with type t = Evar.t list = struct
+module Giveup : Writer with type t = goal list = struct
(* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
- type t = Evar.t list
+ type t = goal list
let put gs = Logical.put (true, gs)
end
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index e7123218b..d26816fa6 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -67,12 +67,21 @@ module Info : sig
end
+module StateStore : Store.S
+type goal = Evar.t
+type goal_with_state
+val drop_state : goal_with_state -> goal
+val get_state : goal_with_state -> StateStore.t
+val goal_with_state : goal -> StateStore.t -> goal_with_state
+val with_empty_state : goal -> goal_with_state
+val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
+
(** Type of proof views: current [evar_map] together with the list of
focused goals. *)
type proofview = {
solution : Evd.evar_map;
- comb : Evar.t list;
- shelf : Evar.t list;
+ comb : goal_with_state list;
+ shelf : goal list;
}
(** {6 Instantiation of the logic monad} *)
@@ -81,7 +90,7 @@ module P : sig
type s = proofview * Environ.env
(** Status (safe/unsafe) * given up *)
- type w = bool * Evar.t list
+ type w = bool * goal list
val wunit : w
val wprod : w -> w -> w
@@ -118,7 +127,7 @@ module Pv : State with type t := proofview
module Solution : State with type t := Evd.evar_map
(** Lens to the list of focused goals. *)
-module Comb : State with type t = Evar.t list
+module Comb : State with type t = goal_with_state list
(** Lens to the global environment. *)
module Env : State with type t := Environ.env
@@ -128,11 +137,11 @@ module Status : Writer with type t := bool
(** Lens to the list of goals which have been shelved during the
execution of the tactic. *)
-module Shelf : State with type t = Evar.t list
+module Shelf : State with type t = goal list
(** Lens to the list of goals which were given up during the execution
of the tactic. *)
-module Giveup : Writer with type t = Evar.t list
+module Giveup : Writer with type t = goal list
(** Lens and utilies pertaining to the info trace *)
module InfoL : sig
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 10be8a842..b61611145 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -973,6 +973,7 @@ TACTIC EXTEND unshelve
| [ "unshelve" tactic1(t) ] ->
[
Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
+ let gls = List.map Proofview.with_empty_state gls in
Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
Proofview.Unsafe.tclSETGOALS (gls @ ogls)
]
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e73a18b79..d42259f2b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1568,7 +1568,8 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
- match clause, prf with
+ let gls = List.map Proofview.with_empty_state gls in
+ match clause, prf with
| Some id, Some p ->
let tac = tclTHENLIST [
Refine.refine ~typecheck:true (fun h -> (h,p));
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 90276951b..73ed70a1a 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -73,6 +73,7 @@ let generic_refine ~typecheck f gl =
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
+ let state = Proofview.Goal.state gl in
(** Save the [future_goals] state to restore them after the
refinement. *)
let prev_future_goals = Evd.future_goals sigma in
@@ -120,6 +121,7 @@ let generic_refine ~typecheck f gl =
(** Select the goals *)
let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+ let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a95e6b941..8284c4939 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1131,6 +1131,7 @@ module Search = struct
let rec result (shelf, ()) i k =
foundone := true;
Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+ let gls = CList.map Proofview.drop_state gls in
let j = List.length gls in
(if !typeclasses_debug > 0 then
Feedback.msg_debug
@@ -1179,7 +1180,7 @@ module Search = struct
(if List.is_empty goals then tclUNIT ()
else
let sigma' = mark_unresolvables sigma goals in
- with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>=
+ with_shelf (Unsafe.tclEVARS sigma' <*> 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, ()) ->
@@ -1272,6 +1273,7 @@ module Search = struct
search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
in
Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+ let gls = CList.map Proofview.drop_state gls in
Proofview.tclEVARMAP >>= fun sigma ->
let j = List.length gls in
(tclDISPATCH (List.init j (fun i -> tac sigma gls i)))
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 695be74bb..0533d0d43 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -334,7 +334,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
let init_refine =
Tacticals.New.tclTHENLIST [
Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
- Proofview.Unsafe.tclNEWGOALS gls;
+ Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
Tactics.New.reduce_after_refine;
]
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 17:41:38 +0000