diff options
| author | Pierre-Marie Pédrot | 2018-09-19 09:13:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-19 09:13:38 +0200 |
| commit | 44b8c4ec9acad33002b080ed0aefb214124db440 (patch) | |
| tree | 96f950c47701467e0c41fa24a7e21f9524977a0b /library | |
| parent | 98aedc543d31ca89428e9789fd76529a7409b7cb (diff) | |
| parent | 736842d4cde09c667837dee8a633ff98ecf6a820 (diff) | |
Merge PR #8447: Cleaning in the retroknowledge
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..6aeae9fd02 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 -> GlobRef.t -> unit val register_inline : Constant.t -> unit |