Merge PR #6676: [proofview] goals come with a state

1 files changed, 2 insertions, 0 deletions

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) <*>