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/cbytegen.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5362f9a814..73620ae578 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -413,7 +413,7 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -let compile_structured_constant cenv sc sz cont = +let compile_structured_constant _cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont @@ -534,7 +534,7 @@ let rec compile_lam env cenv lam sz cont = comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - | Llet (id,def,body) -> + | Llet (_id,def,body) -> compile_lam env cenv def sz (Kpush :: compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) @@ -561,7 +561,7 @@ let rec compile_lam env cenv lam sz cont = | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end - | Lfix ((rec_args, init), (decl, types, bodies)) -> + | Lfix ((rec_args, init), (_decl, types, bodies)) -> let ndef = Array.length types in let rfv = ref empty_fv in let lbl_types = Array.make ndef Label.no in @@ -594,7 +594,7 @@ let rec compile_lam env cenv lam sz cont = (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) - | Lcofix(init, (decl,types,bodies)) -> + | Lcofix(init, (_decl,types,bodies)) -> let ndef = Array.length types in let lbl_types = Array.make ndef Label.no in let lbl_bodies = Array.make ndef Label.no in |