diff options
| author | Maxime Dénès | 2018-09-26 14:55:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 14:55:29 +0200 |
| commit | 5ced288419aed8a622ed2c267e35d9a174facafc (patch) | |
| tree | 2b4f617546ff718e2acad62d35fd7cf3f6d6467a /kernel/names.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 933cefe993..6d33f233e9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -207,7 +207,7 @@ struct let repr mbid = mbid - let to_string (i, s, p) = + let to_string (_i, s, p) = DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = @@ -328,7 +328,7 @@ module ModPath = struct let rec dp = function | MPfile sl -> sl | MPbound (_,_,dp) -> dp - | MPdot (mp,l) -> dp mp + | MPdot (mp,_l) -> dp mp module Self_Hashcons = struct type t = module_path @@ -420,7 +420,7 @@ module KerName = struct let hash kn = let h = kn.refhash in if h < 0 then - let { modpath = mp; dirpath = dp; knlabel = lbl; } = kn in + let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in (* Ensure positivity on all platforms. *) let h = h land 0x3FFFFFFF in @@ -623,8 +623,8 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let inductive_of_constructor (ind, i) = ind -let index_of_constructor (ind, i) = i +let inductive_of_constructor (ind, _i) = ind +let index_of_constructor (_ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = |