aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/g_class.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/g_class.ml4')
-rw-r--r--plugins/ltac/g_class.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 63451210c..0d68d3818 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -21,7 +21,7 @@ let set_transparency cl b =
List.iter (fun r ->
let gr = Smartlocate.global_with_alias r in
let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
- Classes.set_typeclass_transparency ev false b) cl
+ Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [