diff options
Diffstat (limited to 'tactics/g_class.ml4')
| -rw-r--r-- | tactics/g_class.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index c7867a83c..6012088f7 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -17,8 +17,6 @@ END (** Options: depth, debug and transparency settings. *) -open Goptions - let set_transparency cl b = List.iter (fun r -> let gr = Smartlocate.global_with_alias r in |