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/csymtable.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index bb9231d000..8bef6aec42 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -173,7 +173,7 @@ and slot_for_fv env fv = | Some (v, _) -> v end | FVevar evk -> val_of_evar evk - | FVuniv_var idu -> + | FVuniv_var _idu -> assert false and eval_to_patch env (buff,pl,fv) = @@ -192,5 +192,5 @@ and val_of_constr env c = | Some v -> eval_to_patch env (to_memory v) | None -> assert false -let set_transparent_const kn = () (* !?! *) -let set_opaque_const kn = () (* !?! *) +let set_transparent_const _kn = () (* !?! *) +let set_opaque_const _kn = () (* !?! *) |