diff options
Diffstat (limited to 'plugins/ltac/evar_tactics.ml')
| -rw-r--r-- | plugins/ltac/evar_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 73490a2dfd..b0277e9cc2 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -99,7 +99,7 @@ let let_evar name typ = let hget_evar n = let open EConstr in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in |