diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 74b075f4a5..482a2f3a3c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function let list_of_mp mp = list_of_mp [] mp let string_of_kn kn = - let (mp,_dp,l) = KerName.repr kn in + let (mp,l) = KerName.repr kn in let mp = list_of_mp mp in String.concat "_" mp ^ "_" ^ string_of_label l |