From ab2560233f2e6fc8c26853af6991533d8d335e16 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 11:34:32 +0200
Subject: Retroknowledge: remove the (unused) by clause

---
 library/global.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/global.ml')

diff --git a/library/global.ml b/library/global.ml
index e833f71142..5872126a12 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -271,8 +271,8 @@ let with_global f =
     push_context_set false ctx; a
 
 (* spiwack: register/unregister functions for retroknowledge *)
-let register field value by_clause =
-  globalize0 (Safe_typing.register field value by_clause)
+let register field value =
+  globalize0 (Safe_typing.register field value)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
 
-- 
cgit v1.2.3