diff options
Diffstat (limited to 'plugins/ltac/g_class.ml4')
| -rw-r--r-- | plugins/ltac/g_class.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 23ce368ee..dd5307638 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -102,18 +102,18 @@ let rec eq_constr_mod_evars sigma x y = | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y let progress_evars t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let check = - Proofview.Goal.enter { enter = begin fun gl' -> + Proofview.Goal.enter begin fun gl' -> let sigma = Tacmach.New.project gl' in let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars sigma concl newconcl then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") else Proofview.tclUNIT () - end } + end in t <*> check - end } + end TACTIC EXTEND progress_evars [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] |