diff options
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1160884c3..c741610a3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -75,10 +75,10 @@ let rec eq_constr_mod_evars x y = | _, _ -> compare_constr eq_constr_mod_evars x y let progress_evars t = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let check = - Proofview.Goal.enter begin fun gl' -> + Proofview.Goal.nf_enter begin fun gl' -> let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars concl newconcl then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") |