aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_instruct.h
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/coq_instruct.h')
-rw-r--r--kernel/byterun/coq_instruct.h67
1 files changed, 0 insertions, 67 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
deleted file mode 100644
index c7abedaed6..0000000000
--- a/kernel/byterun/coq_instruct.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/***********************************************************************/
-/* */
-/* Coq Compiler */
-/* */
-/* Benjamin Gregoire, projets Logical and Cristal */
-/* INRIA Rocquencourt */
-/* */
-/* */
-/***********************************************************************/
-
-#ifndef _COQ_INSTRUCT_
-#define _COQ_INSTRUCT_
-
-/* Nota: this list of instructions is parsed to produce derived files */
-/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */
-/* and alone on lines starting by two spaces. */
-/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */
-/* with the arity of the instruction and maybe coq_tcode_of_code. */
-
-enum instructions {
- ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
- PUSH,
- PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4,
- PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC,
- POP,
- ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
- PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
- PUSH_RETADDR,
- APPLY, APPLY1, APPLY2, APPLY3, APPLY4,
- APPTERM, APPTERM1, APPTERM2, APPTERM3,
- RETURN, RESTART, GRAB, GRABREC,
- CLOSURE, CLOSUREREC, CLOSURECOFIX,
- OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
- PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2,
- PUSHOFFSETCLOSURE,
- GETGLOBAL, PUSHGETGLOBAL,
- MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4,
- SWITCH, PUSHFIELDS,
- GETFIELD0, GETFIELD1, GETFIELD,
- SETFIELD0, SETFIELD1, SETFIELD,
- PROJ,
- ENSURESTACKCAPACITY,
- CONST0, CONST1, CONST2, CONST3, CONSTINT,
- PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
- ACCUMULATE,
- MAKESWITCHBLOCK, MAKEACCU, MAKEPROD,
-/* spiwack: */
- BRANCH,
- CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63,
- CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63,
- CHECKMULINT63, CHECKMULCINT63,
- CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63,
- CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63,
- CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63,
- CHECKLSLINT63CONST1, CHECKLSRINT63CONST1,
-
- CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63,
- CHECKCOMPAREINT63,
-
- CHECKHEAD0INT63, CHECKTAIL0INT63,
-
- ISINT, AREINT2,
-
- STOP
-};
-
-#endif /* _COQ_INSTRUCT_ */