aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_fix_code.h
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-02-04 17:22:36 +0100
committerPierre-Marie Pédrot2019-02-04 17:22:36 +0100
commitc70412ec8b0bb34b7a5607c07d34607a147d834c (patch)
tree0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /kernel/byterun/coq_fix_code.h
parent720ee2730684cc289cef588482323d177e0bea59 (diff)
parent191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff)
Merge PR #6914: Primitive integers
Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
Diffstat (limited to 'kernel/byterun/coq_fix_code.h')
-rw-r--r--kernel/byterun/coq_fix_code.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 638d6b5ab5..5a233e6178 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -29,6 +29,7 @@ void init_arity();
value coq_tcode_of_code(value code);
value coq_makeaccu (value i);
value coq_pushpop (value i);
+value coq_accucond (value i);
value coq_is_accumulate_code(value code);
#endif /* _COQ_FIX_CODE_ */