diff options
| author | coqbot-app[bot] | 2020-11-13 15:28:53 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-13 15:28:53 +0000 |
| commit | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (patch) | |
| tree | 0feb6d52dff924f53d5f39d824816f0ee77e50e5 /kernel/nativecode.mli | |
| parent | 51e759fb2ff92dd89ab4823ddea3ea81be7f8046 (diff) | |
| parent | 9cf424839dd7aa1b2ed26e2ed12c9c618969e3b0 (diff) | |
Merge PR #13358: Merge the Linked / LinkedInteractive native link information constructors
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/nativecode.mli')
| -rw-r--r-- | kernel/nativecode.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 913b3843c2..aab6e1d4a0 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -50,7 +50,6 @@ val get_proj : symbols -> int -> inductive * int val get_symbols : unit -> symbols -type code_location_update type code_location_updates type linkable_code = global list * code_location_updates |