diff options
Diffstat (limited to 'tactics/g_class.ml4')
| -rw-r--r-- | tactics/g_class.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 6012088f7..1e666e5a5 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -11,6 +11,8 @@ open Misctypes open Class_tactics +DECLARE PLUGIN "g_class" + TACTIC EXTEND progress_evars [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] END |