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/nativeconv.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c75dde843e..054b6a2d17 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -25,9 +25,9 @@ let rec conv_val env pb lvl v1 v2 cu = | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in conv_val env CONV (lvl+1) (f1 v) (f2 v) cu - | Vfun f1, _ -> + | Vfun _f1, _ -> conv_val env CONV lvl v1 (fun x -> v2 x) cu - | _, Vfun f2 -> + | _, Vfun _f2 -> conv_val env CONV lvl (fun x -> v1 x) v2 cu | Vaccu k1, Vaccu k2 -> conv_accu env pb lvl k1 k2 cu @@ -110,7 +110,7 @@ and conv_atom env pb lvl a1 a2 cu = else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu - | Aprod(_,d1,c1), Aprod(_,d2,c2) -> + | Aprod(_,d1,_c1), Aprod(_,d2,_c2) -> let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu |