aboutsummaryrefslogtreecommitdiff
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml6
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 = () (* !?! *)