diff options
Diffstat (limited to 'tactics/g_class.ml4')
| -rw-r--r-- | tactics/g_class.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index e0c1f671fd..766593543c 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -14,7 +14,7 @@ open Class_tactics DECLARE PLUGIN "g_class" TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] + [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] END (** Options: depth, debug and transparency settings. *) |