File: coq_fix_code.h

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (31 lines) | stat: -rw-r--r-- 1,151 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
/***********************************************************************/
/*                                                                     */
/*                           Coq Compiler                              */
/*                                                                     */
/*        Benjamin Gregoire, projets Logical and Cristal               */
/*                        INRIA Rocquencourt                           */
/*                                                                     */
/*                                                                     */
/***********************************************************************/


#ifndef _COQ_FIX_CODE_
#define _COQ_FIX_CODE_

#include <caml/mlvalues.h>
void * coq_stat_alloc (asize_t sz);

#ifdef THREADED_CODE
void coq_init_thread_code(void ** instr_table, void * instr_base);
#endif /*  THREADED_CODE */

extern code_t accumulate;

int coq_is_instruction(opcode_t, opcode_t);
value coq_tcode_of_code(value code);
value coq_accumulate(value);
value coq_makeaccu (value i);
value coq_pushpop (value i);
value coq_accucond (value i);

#endif /* _COQ_FIX_CODE_ */