aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/byterun/coq_values.c
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-10-14 10:44:44 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-10-14 10:44:44 +0200
commit4a1234459472c5fbb0d0467217972f247c054832 (patch)
treee14b407117227615ea07e48c82f3b61f44a19123 /kernel/byterun/coq_values.c
parentf617aeef08441e83b13f839ce767b840fddbcf7d (diff)
Remove some unused variables.
Diffstat (limited to 'kernel/byterun/coq_values.c')
-rw-r--r--kernel/byterun/coq_values.c1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b27..528babebf 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
value coq_kind_of_closure(value v) {
opcode_t * c;
- int res;
int is_app = 0;
c = Code_val(v);
if (Is_instruction(c, GRAB)) return Val_int(0);