aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/global.ml')
-rw-r--r--library/global.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml
index 8b61c9a4a..c2c42159b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -68,7 +68,7 @@ let add_module = add_thing (fun _ -> add_module) ()
let add_constraints c = global_env := add_constraints c !global_env
-
+let set_engagement c = global_env := set_engagement c !global_env
let start_module id params mtyo =
let l = label_of_id id in