diff options
Diffstat (limited to 'plugins/ltac/g_class.ml4')
| -rw-r--r-- | plugins/ltac/g_class.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 23ce368eea..905cfd02a6 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,10 +8,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API open Class_tactics open Stdarg open Tacarg -open Names DECLARE PLUGIN "g_class" @@ -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) ] |