diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 2 | ||||
| -rw-r--r-- | proofs/refine.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 78fe850bc..24f570f01 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -434,7 +434,7 @@ module V82 = struct CList.nth evl (n-1) in let env = Evd.evar_filtered_env evi in - let rawc = Constrintern.intern_constr env com in + let rawc = Constrintern.intern_constr env sigma com in let ltac_vars = Glob_ops.empty_lvar in let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma diff --git a/proofs/refine.ml b/proofs/refine.ml index 4469f2772..50fd1c472 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -75,6 +75,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 @@ -122,6 +123,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) <*> |