diff options
| author | Vincent Laporte | 2018-09-07 11:34:32 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | ab2560233f2e6fc8c26853af6991533d8d335e16 (patch) | |
| tree | a5712bb6310eb819f620a504b62533adf240cd94 /library | |
| parent | 4be2dd481c783bed7c09086b647d860e42b7ea9f (diff) | |
Retroknowledge: remove the (unused) by clause
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 4 | ||||
| -rw-r--r-- | library/global.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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) diff --git a/library/global.mli b/library/global.mli index 2819c187ed..1708976222 100644 --- a/library/global.mli +++ b/library/global.mli @@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) val register : - Retroknowledge.field -> Constr.constr -> Constr.constr -> unit + Retroknowledge.field -> Constr.constr -> unit val register_inline : Constant.t -> unit |