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/mod_subst.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f1d08ef6dd..bff3092655 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -319,12 +319,12 @@ let subst_con sub cst = let subst_con_kn sub con = subst_con sub (con,Univ.Instance.empty) -let subst_pcon sub (con,u as pcon) = - try let con', can = subst_con0 sub pcon in +let subst_pcon sub (_con,u as pcon) = + try let con', _can = subst_con0 sub pcon in con',u with No_subst -> pcon -let subst_pcon_term sub (con,u as pcon) = +let subst_pcon_term sub (_con,u as pcon) = try let con', can = subst_con0 sub pcon in (con',u), can with No_subst -> pcon, mkConstU pcon @@ -441,7 +441,7 @@ let replace_mp_in_kn mpfrom mpto kn = let rec mp_in_mp mp mp1 = match mp1 with | _ when ModPath.equal mp1 mp -> true - | MPdot (mp2,l) -> mp_in_mp mp mp2 + | MPdot (mp2,_l) -> mp_in_mp mp mp2 | _ -> false let subset_prefixed_by mp resolver = |