diff options
Diffstat (limited to 'ltac/g_class.ml4')
| -rw-r--r-- | ltac/g_class.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index a28132a4b..ca9537c82 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -13,6 +13,7 @@ open Class_tactics open Pltac open Stdarg open Tacarg +open Names DECLARE PLUGIN "g_class" |