diff options
| author | Vincent Laporte | 2018-09-07 17:34:11 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-14 07:51:17 +0000 |
| commit | 2ec78477c720ba3a5343b49f25cfa9c1639adbba (patch) | |
| tree | ed8129ee7206bcb32c5e7d41830caf22b7cc2254 /library | |
| parent | 42bed627c4a1c5a1ecf59d4865fc872b5eee7290 (diff) | |
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index 1708976222..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 -> unit + Retroknowledge.field -> GlobRef.t -> unit val register_inline : Constant.t -> unit |