aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_values.c
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/coq_values.c')
-rw-r--r--kernel/byterun/coq_values.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index e05f3fb82e..3613bc07a6 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -39,7 +39,7 @@ value coq_closure_arity(value clos) {
if (Is_instruction(c,RESTART)) {
c++;
if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
- else {
+ else {
if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
return Val_int(1);
}