aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-18 12:19:12 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-18 12:19:12 +0000
commitf3eaf2869e84c942d56a7fe0cc459d9943e4b059 (patch)
tree4a67e700f35e74324cece25f50325758e43dcb03 /kernel/cbytecodes.mli
parent0e1b31da1546b7ac0dd3664e73ba05127320bed9 (diff)
Nettoyage de code en vue de la release. Plus de Warning: Unused
Variable, et plus de trucs useless qui traƮnaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.mli')
-rw-r--r--kernel/cbytecodes.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 86b465543..c24b5a530 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -132,8 +132,6 @@ type comp_env = {
val draw_instr : bytecodes -> unit
-val string_of_instr : bytecodes -> string
-
(*spiwack: moved this here because I needed it for retroknowledge *)