diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 551c316e79..4148102f61 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -393,10 +393,13 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in let gen_eq_tac = - Proofview.V82.tactic ~nf_evars:false begin fun s -> + let open Proofview.Notations in + Proofview.Goal.enter begin fun s -> + let sigma = Proofview.Goal.sigma s in let open Evd in - let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in - apply_type new_concl [erefl] { s with sigma } + let sigma = merge_universe_context sigma (evar_universe_context (project gl)) in + Proofview.Unsafe.tclEVARS sigma <*> + Tactics.apply_type ~typecheck:true new_concl [erefl] end in gen_eq_tac, eq_ty, gl in |