[vm] Untabify the VM C code.

This is a follow up of #11010 ; I've realized that for example in #11123
a large part of the patch is detabification as indeed the files are
mixed in tabs/space style so developers are forced to do the cleanup
each time they work on them.

Command used:

```
for i in `find . -name '*.c' -or -name '*.h'; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```

Checked empty diff with `git diff --ignore-all-space`

6 files changed, 677 insertions, 677 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 931b509f48..306643f758 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -12,7 +12,7 @@
    for fast computation of bounded (31bits) integers */
 
 #include <stdio.h>
-#include <stdlib.h> 
+#include <stdlib.h>
 #include <stdint.h>
 #include <caml/config.h>
 #include <caml/misc.h>
@@ -42,7 +42,7 @@ void init_arity () {
     arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
-    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
+    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
     arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
     arity[LTFLOAT]=arity[LEFLOAT]=
     arity[ISINT]=arity[AREINT2]=0;
@@ -76,7 +76,7 @@ void init_arity () {
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
   arity[PROJ]=2;
-  /* instruction with four operands */ 
+  /* instruction with four operands */
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
   arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
@@ -134,7 +134,7 @@ value coq_is_accumulate_code(value code){
 
 #ifdef ARCH_BIG_ENDIAN
 #define Reverse_32(dst,src) {                                               \
-  char * _p, * _q;							    \
+  char * _p, * _q;                                                          \
   char _a, _b;                                                              \
   _p = (char *) (src);                                                      \
   _q = (char *) (dst);                                                      \
@@ -159,9 +159,9 @@ value coq_tcode_of_code (value code) {
   q = coq_stat_alloc(len);
   Code_val(res) = q;
   len /= sizeof(opcode_t);
-  for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {  
+  for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
     opcode_t instr;
-    COPY32(&instr,p); 
+    COPY32(&instr,p);
     p++;
     if (instr < 0 || instr > STOP){
       instr = STOP;
@@ -183,7 +183,7 @@ value coq_tcode_of_code (value code) {
       for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
     } else {
       uint32_t i, ar;
-      ar = arity[instr]; 
+      ar = arity[instr];
       for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
     }
   }
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index f06275862c..38eda4d11f 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -37,8 +37,8 @@ CAMLextern void minor_collection (void);
 
 #define Make_header(wosize, tag, color)                                 \
   (((header_t) (((header_t) (wosize) << 10)                             \
-		+ (color)                                               \
-		+ (tag_t) (tag)))   					\
+                + (color)                                               \
+                + (tag_t) (tag)))                                       \
    )
 #endif
 
@@ -53,7 +53,7 @@ CAMLextern void minor_collection (void);
   }                                                                     \
   Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
   (result) = Val_hp (young_ptr);                                        \
-  }while(0) 
+  }while(0)
 
 
 #endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ca1308696c..b78643e226 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -21,8 +21,8 @@
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
-#include "coq_memory.h" 
-#include "coq_values.h" 
+#include "coq_memory.h"
+#include "coq_values.h"
 #include "coq_float64.h"
 
 #ifdef ARCH_SIXTYFOUR
@@ -49,7 +49,7 @@ sp is a local copy of the global variable extern_sp. */
 
 
 #ifdef THREADED_CODE
-#  define Instruct(name) coq_lbl_##name: 
+#  define Instruct(name) coq_lbl_##name:
 #  if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
 #    define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0)
 #  else
@@ -59,22 +59,22 @@ sp is a local copy of the global variable extern_sp. */
 #  ifdef DEBUG
 #    define Next goto next_instr
 #  else
-#    define Next goto *(void *)(coq_jumptbl_base + *pc++)  
+#    define Next goto *(void *)(coq_jumptbl_base + *pc++)
 #  endif
-#else 
+#else
 #  define Instruct(name) case name:
 #  define Next break
-#endif 
+#endif
 
 /* #define _COQ_DEBUG_ */
 
-#ifdef _COQ_DEBUG_ 
+#ifdef _COQ_DEBUG_
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
 #   define print_int(i)   /*if (drawinstr)*/ printf("%d\n",i)
 #   define print_lint(i)  /*if (drawinstr)*/ printf("%ld\n",i)
-# else 
-#   define print_instr(s) 
-#   define print_int(i) 
+# else
+#   define print_instr(s)
+#   define print_int(i)
 #   define print_lint(i)
 #endif
 
@@ -95,7 +95,7 @@ if (sp - num_args < coq_stack_threshold) {                                     \
    Some compilers underestimate the use of the local variables representing
    the abstract machine registers, and don't put them in hardware registers,
    which slows down the interpreter considerably.
-   For GCC, Xavier Leroy have hand-assigned hardware registers for 
+   For GCC, Xavier Leroy have hand-assigned hardware registers for
    several architectures.
 */
 
@@ -171,11 +171,11 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 
 #define CheckPrimArgs(cond, apply_lbl) do{         \
     if (cond) pc++;                                \
-    else{					   \
-      *--sp=accu;				   \
-      accu = Field(coq_global_data, *pc++);	   \
+    else{                                          \
+      *--sp=accu;                                  \
+      accu = Field(coq_global_data, *pc++);        \
       goto apply_lbl;                              \
-    }						   \
+    }                                              \
   }while(0)
 
 #define CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1)
@@ -238,7 +238,7 @@ value coq_interprete
   static void * coq_jumptable[] = {
 #    include "coq_jumptbl.h"
   };
-#else 
+#else
   opcode_t curr_instr;
 #endif
   print_instr("Enter Interpreter");
@@ -269,193 +269,193 @@ value coq_interprete
     switch(curr_instr) {
 #endif
 /* Basic stack operations */
-      
+
       Instruct(ACC0){
-	print_instr("ACC0");
-	accu = sp[0]; Next;
+        print_instr("ACC0");
+        accu = sp[0]; Next;
       }
       Instruct(ACC1){
-	print_instr("ACC1");
-	accu = sp[1]; Next;
+        print_instr("ACC1");
+        accu = sp[1]; Next;
       }
       Instruct(ACC2){
-	print_instr("ACC2");
-	accu = sp[2]; Next;
+        print_instr("ACC2");
+        accu = sp[2]; Next;
       }
       Instruct(ACC3){
-	print_instr("ACC3");
-	accu = sp[3]; Next;
+        print_instr("ACC3");
+        accu = sp[3]; Next;
       }
       Instruct(ACC4){
-	print_instr("ACC4");
-	accu = sp[4]; Next;
+        print_instr("ACC4");
+        accu = sp[4]; Next;
       }
       Instruct(ACC5){
-	print_instr("ACC5");
-	accu = sp[5]; Next;
+        print_instr("ACC5");
+        accu = sp[5]; Next;
       }
       Instruct(ACC6){
-	print_instr("ACC6");
-	accu = sp[6]; Next;
+        print_instr("ACC6");
+        accu = sp[6]; Next;
       }
       Instruct(ACC7){
-	print_instr("ACC7");
+        print_instr("ACC7");
         accu = sp[7]; Next;
-      }      
+      }
       Instruct(PUSH){
-	print_instr("PUSH");
-	*--sp = accu; Next;
+        print_instr("PUSH");
+        *--sp = accu; Next;
       }
       Instruct(PUSHACC0) {
-	print_instr("PUSHACC0");
+        print_instr("PUSHACC0");
         *--sp = accu; Next;
       }
       Instruct(PUSHACC1){
-	print_instr("PUSHACC1");
+        print_instr("PUSHACC1");
         *--sp = accu; accu = sp[1]; Next;
       }
       Instruct(PUSHACC2){
-	print_instr("PUSHACC2");
+        print_instr("PUSHACC2");
         *--sp = accu; accu = sp[2]; Next;
       }
       Instruct(PUSHACC3){
-	print_instr("PUSHACC3");
-	*--sp = accu; accu = sp[3]; Next;
+        print_instr("PUSHACC3");
+        *--sp = accu; accu = sp[3]; Next;
       }
       Instruct(PUSHACC4){
-	print_instr("PUSHACC4");
-	*--sp = accu; accu = sp[4]; Next;
+        print_instr("PUSHACC4");
+        *--sp = accu; accu = sp[4]; Next;
       }
       Instruct(PUSHACC5){
-	print_instr("PUSHACC5");
-	*--sp = accu; accu = sp[5]; Next;
+        print_instr("PUSHACC5");
+        *--sp = accu; accu = sp[5]; Next;
       }
       Instruct(PUSHACC6){
-	print_instr("PUSHACC5");
-	*--sp = accu; accu = sp[6]; Next;
+        print_instr("PUSHACC5");
+        *--sp = accu; accu = sp[6]; Next;
       }
       Instruct(PUSHACC7){
-	print_instr("PUSHACC7");
-	*--sp = accu; accu = sp[7]; Next;
+        print_instr("PUSHACC7");
+        *--sp = accu; accu = sp[7]; Next;
       }
       Instruct(PUSHACC){
-	print_instr("PUSHACC");
-	*--sp = accu;
+        print_instr("PUSHACC");
+        *--sp = accu;
       }
       /* Fallthrough */
-      
+
       Instruct(ACC){
-	print_instr("ACC");
-	accu = sp[*pc++];
+        print_instr("ACC");
+        accu = sp[*pc++];
         Next;
       }
-      
+
       Instruct(POP){
-	print_instr("POP");
-	sp += *pc++;
-	Next;
+        print_instr("POP");
+        sp += *pc++;
+        Next;
       }
       /* Access in heap-allocated environment */
-      
+
       Instruct(ENVACC1){
-	print_instr("ENVACC1");
-	accu = Field(coq_env, 1); Next;
+        print_instr("ENVACC1");
+        accu = Field(coq_env, 1); Next;
       }
       Instruct(ENVACC2){
-	print_instr("ENVACC2");
-	accu = Field(coq_env, 2); Next;
+        print_instr("ENVACC2");
+        accu = Field(coq_env, 2); Next;
       }
       Instruct(ENVACC3){
-	print_instr("ENVACC3");
-	accu = Field(coq_env, 3); Next;
+        print_instr("ENVACC3");
+        accu = Field(coq_env, 3); Next;
       }
       Instruct(ENVACC4){
-	print_instr("ENVACC4");
-	accu = Field(coq_env, 4); Next;
+        print_instr("ENVACC4");
+        accu = Field(coq_env, 4); Next;
       }
       Instruct(PUSHENVACC1){
-	print_instr("PUSHENVACC1");
-	*--sp = accu; accu = Field(coq_env, 1); Next;
+        print_instr("PUSHENVACC1");
+        *--sp = accu; accu = Field(coq_env, 1); Next;
       }
       Instruct(PUSHENVACC2){
-	print_instr("PUSHENVACC2");
-	*--sp = accu; accu = Field(coq_env, 2); Next;
+        print_instr("PUSHENVACC2");
+        *--sp = accu; accu = Field(coq_env, 2); Next;
       }
       Instruct(PUSHENVACC3){
-	print_instr("PUSHENVACC3");
-	*--sp = accu; accu = Field(coq_env, 3); Next;
+        print_instr("PUSHENVACC3");
+        *--sp = accu; accu = Field(coq_env, 3); Next;
       }
       Instruct(PUSHENVACC4){
-	print_instr("PUSHENVACC4");
-	*--sp = accu; accu = Field(coq_env, 4); Next;
+        print_instr("PUSHENVACC4");
+        *--sp = accu; accu = Field(coq_env, 4); Next;
       }
       Instruct(PUSHENVACC){
-	print_instr("PUSHENVACC");
-	*--sp = accu;
+        print_instr("PUSHENVACC");
+        *--sp = accu;
       }
       /* Fallthrough */
       Instruct(ENVACC){
-	print_instr("ENVACC");
-	print_int(*pc);
-	accu = Field(coq_env, *pc++);
+        print_instr("ENVACC");
+        print_int(*pc);
+        accu = Field(coq_env, *pc++);
         Next;
       }
       /* Function application */
-      
+
       Instruct(PUSH_RETADDR) {
-	print_instr("PUSH_RETADDR");
-	sp -= 3;
-	sp[0] = (value) (pc + *pc);
-	sp[1] = coq_env;
-	sp[2] = Val_long(coq_extra_args);
-	coq_extra_args = 0;
-	pc++;
-	Next;
+        print_instr("PUSH_RETADDR");
+        sp -= 3;
+        sp[0] = (value) (pc + *pc);
+        sp[1] = coq_env;
+        sp[2] = Val_long(coq_extra_args);
+        coq_extra_args = 0;
+        pc++;
+        Next;
       }
       Instruct(APPLY) {
-	print_instr("APPLY");
-	coq_extra_args = *pc - 1;
-	pc = Code_val(accu);
-	coq_env = accu;
-	goto check_stack;
+        print_instr("APPLY");
+        coq_extra_args = *pc - 1;
+        pc = Code_val(accu);
+        coq_env = accu;
+        goto check_stack;
       }
       Instruct(APPLY1) {
         value arg1;
       apply1:
-	print_instr("APPLY1");
+        print_instr("APPLY1");
         arg1 = sp[0];
-	sp -= 3;
-	sp[0] = arg1;
-	sp[1] = (value)pc;
-	sp[2] = coq_env;
-	sp[3] = Val_long(coq_extra_args);
-	print_instr("call stack=");
-	print_lint(sp[1]);
-	print_lint(sp[2]);
-	print_lint(sp[3]);
-	pc = Code_val(accu);
-	coq_env = accu;
-	coq_extra_args = 0;
-	goto check_stack;
+        sp -= 3;
+        sp[0] = arg1;
+        sp[1] = (value)pc;
+        sp[2] = coq_env;
+        sp[3] = Val_long(coq_extra_args);
+        print_instr("call stack=");
+        print_lint(sp[1]);
+        print_lint(sp[2]);
+        print_lint(sp[3]);
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args = 0;
+        goto check_stack;
       }
 
       Instruct(APPLY2) {
         value arg1;
         value arg2;
       apply2:
-	print_instr("APPLY2");
+        print_instr("APPLY2");
         arg1 = sp[0];
         arg2 = sp[1];
-	sp -= 3;
-	sp[0] = arg1;
-	sp[1] = arg2;
-	sp[2] = (value)pc;
-	sp[3] = coq_env;
-	sp[4] = Val_long(coq_extra_args);
-	pc = Code_val(accu);
-	coq_env = accu;
-	coq_extra_args = 1;
-	goto check_stack;
+        sp -= 3;
+        sp[0] = arg1;
+        sp[1] = arg2;
+        sp[2] = (value)pc;
+        sp[3] = coq_env;
+        sp[4] = Val_long(coq_extra_args);
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args = 1;
+        goto check_stack;
       }
 
       Instruct(APPLY3) {
@@ -463,21 +463,21 @@ value coq_interprete
         value arg2;
         value arg3;
       apply3:
-	print_instr("APPLY3");
+        print_instr("APPLY3");
         arg1 = sp[0];
         arg2 = sp[1];
         arg3 = sp[2];
-	sp -= 3;
-	sp[0] = arg1;
-	sp[1] = arg2;
-	sp[2] = arg3;
-	sp[3] = (value)pc;
-	sp[4] = coq_env;
-	sp[5] = Val_long(coq_extra_args);
-	pc = Code_val(accu);
-	coq_env = accu;
-	coq_extra_args = 2;
-	goto check_stack;
+        sp -= 3;
+        sp[0] = arg1;
+        sp[1] = arg2;
+        sp[2] = arg3;
+        sp[3] = (value)pc;
+        sp[4] = coq_env;
+        sp[5] = Val_long(coq_extra_args);
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args = 2;
+        goto check_stack;
       }
 
        Instruct(APPLY4) {
@@ -501,15 +501,15 @@ value coq_interprete
       }
 
      /* Stack checks */
-      
+
     check_stack:
       print_instr("check_stack");
       CHECK_STACK(0);
       /* We also check for signals */
       if (caml_signals_are_pending) {
-	/* If there's a Ctrl-C, we reset the vm */
-	if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
-	caml_process_pending_signals();
+        /* If there's a Ctrl-C, we reset the vm */
+        if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+        caml_process_pending_signals();
       }
       Next;
 
@@ -524,460 +524,460 @@ value coq_interprete
       }
 
       Instruct(APPTERM) {
-	int nargs = *pc++;
-	int slotsize = *pc;
-	value * newsp;
-	int i;
-	print_instr("APPTERM");
-	/* Slide the nargs bottom words of the current frame to the top
-	   of the frame, and discard the remainder of the frame */
-	newsp = sp + slotsize - nargs;
-	for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
-	sp = newsp;
-	pc = Code_val(accu);
-	coq_env = accu;
-	coq_extra_args += nargs - 1;
-	goto check_stack;
+        int nargs = *pc++;
+        int slotsize = *pc;
+        value * newsp;
+        int i;
+        print_instr("APPTERM");
+        /* Slide the nargs bottom words of the current frame to the top
+           of the frame, and discard the remainder of the frame */
+        newsp = sp + slotsize - nargs;
+        for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
+        sp = newsp;
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args += nargs - 1;
+        goto check_stack;
       }
       Instruct(APPTERM1) {
-	value arg1 = sp[0];
-	print_instr("APPTERM1");
-	sp = sp + *pc - 1;
-	sp[0] = arg1;
-	pc = Code_val(accu);
-	coq_env = accu;
-	goto check_stack;
+        value arg1 = sp[0];
+        print_instr("APPTERM1");
+        sp = sp + *pc - 1;
+        sp[0] = arg1;
+        pc = Code_val(accu);
+        coq_env = accu;
+        goto check_stack;
       }
       Instruct(APPTERM2) {
-	value arg1 = sp[0];
-	value arg2 = sp[1];
-	print_instr("APPTERM2");
-	sp = sp + *pc - 2;
-	sp[0] = arg1;
-	sp[1] = arg2;
-	pc = Code_val(accu);
-	print_lint(accu);
-	coq_env = accu;
-	coq_extra_args += 1;
-	goto check_stack;
+        value arg1 = sp[0];
+        value arg2 = sp[1];
+        print_instr("APPTERM2");
+        sp = sp + *pc - 2;
+        sp[0] = arg1;
+        sp[1] = arg2;
+        pc = Code_val(accu);
+        print_lint(accu);
+        coq_env = accu;
+        coq_extra_args += 1;
+        goto check_stack;
       }
       Instruct(APPTERM3) {
-	value arg1 = sp[0];
-	value arg2 = sp[1];
-	value arg3 = sp[2];
-	print_instr("APPTERM3");
-	sp = sp + *pc - 3;
-	sp[0] = arg1;
-	sp[1] = arg2;
-	sp[2] = arg3;
-	pc = Code_val(accu);
-	coq_env = accu;
-	coq_extra_args += 2;
-	goto check_stack;
-      }
-      
+        value arg1 = sp[0];
+        value arg2 = sp[1];
+        value arg3 = sp[2];
+        print_instr("APPTERM3");
+        sp = sp + *pc - 3;
+        sp[0] = arg1;
+        sp[1] = arg2;
+        sp[2] = arg3;
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args += 2;
+        goto check_stack;
+      }
+
       Instruct(RETURN) {
-	print_instr("RETURN");
-	print_int(*pc);
-	sp += *pc++;
-	print_instr("stack=");
-	print_lint(sp[0]);
-	print_lint(sp[1]);
-	print_lint(sp[2]);
-	if (coq_extra_args > 0) {
-	  print_instr("extra args > 0");
-	  print_lint(coq_extra_args);
-	  coq_extra_args--;
-	  pc = Code_val(accu);
-	  coq_env = accu;
-	} else {
-	  print_instr("extra args = 0");
-	  pc = (code_t)(sp[0]);
-	  coq_env = sp[1];
-	  coq_extra_args = Long_val(sp[2]);
-	  sp += 3;
-	}
-	Next;
-      }
-      
+        print_instr("RETURN");
+        print_int(*pc);
+        sp += *pc++;
+        print_instr("stack=");
+        print_lint(sp[0]);
+        print_lint(sp[1]);
+        print_lint(sp[2]);
+        if (coq_extra_args > 0) {
+          print_instr("extra args > 0");
+          print_lint(coq_extra_args);
+          coq_extra_args--;
+          pc = Code_val(accu);
+          coq_env = accu;
+        } else {
+          print_instr("extra args = 0");
+          pc = (code_t)(sp[0]);
+          coq_env = sp[1];
+          coq_extra_args = Long_val(sp[2]);
+          sp += 3;
+        }
+        Next;
+      }
+
       Instruct(RESTART) {
-	int num_args = Wosize_val(coq_env) - 2;
-	int i;
-	print_instr("RESTART");
+        int num_args = Wosize_val(coq_env) - 2;
+        int i;
+        print_instr("RESTART");
         CHECK_STACK(num_args);
-	sp -= num_args;
-	for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
-	coq_env = Field(coq_env, 1);
-	coq_extra_args += num_args;
-	Next;
+        sp -= num_args;
+        for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
+        coq_env = Field(coq_env, 1);
+        coq_extra_args += num_args;
+        Next;
       }
-      
+
       Instruct(GRAB) {
-	int required = *pc++;
-	print_instr("GRAB");
-	/*	printf("GRAB %d\n",required); */
-	if (coq_extra_args >= required) {
-	  coq_extra_args -= required;
-	} else {
-	  mlsize_t num_args, i;
-	  num_args = 1 + coq_extra_args; /* arg1 + extra args */
-          Alloc_small(accu, num_args + 2, Closure_tag); 
-	  Field(accu, 1) = coq_env;
-	  for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
-	  Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
-	  sp += num_args;
-	  pc = (code_t)(sp[0]);
-	  coq_env = sp[1];
-	  coq_extra_args = Long_val(sp[2]);
-	  sp += 3;
-	}
-	Next;
-      }
-
-      Instruct(GRABREC) { 
-	int rec_pos = *pc++; /* commence a zero */
-	print_instr("GRABREC");
-	if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
-	  pc++;/* On saute le Restart */
-	} else {
-	  if (coq_extra_args < rec_pos) {
+        int required = *pc++;
+        print_instr("GRAB");
+        /*      printf("GRAB %d\n",required); */
+        if (coq_extra_args >= required) {
+          coq_extra_args -= required;
+        } else {
+          mlsize_t num_args, i;
+          num_args = 1 + coq_extra_args; /* arg1 + extra args */
+          Alloc_small(accu, num_args + 2, Closure_tag);
+          Field(accu, 1) = coq_env;
+          for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+          Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+          sp += num_args;
+          pc = (code_t)(sp[0]);
+          coq_env = sp[1];
+          coq_extra_args = Long_val(sp[2]);
+          sp += 3;
+        }
+        Next;
+      }
+
+      Instruct(GRABREC) {
+        int rec_pos = *pc++; /* commence a zero */
+        print_instr("GRABREC");
+        if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
+          pc++;/* On saute le Restart */
+        } else {
+          if (coq_extra_args < rec_pos) {
             /* Partial application */
-	    mlsize_t num_args, i;
-	    num_args = 1 + coq_extra_args; /* arg1 + extra args */
-	    Alloc_small(accu, num_args + 2, Closure_tag); 
-	    Field(accu, 1) = coq_env;
-	    for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
-	    Code_val(accu) = pc - 3; 
-	    sp += num_args;
-	    pc = (code_t)(sp[0]);
-	    coq_env = sp[1];
-	    coq_extra_args = Long_val(sp[2]);
-	    sp += 3;
-	  } else {
-	    /* The recursif argument is an accumulator */
-	    mlsize_t num_args, i;
-	    /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
-	    Alloc_small(accu, rec_pos + 2, Closure_tag); 
-	    Field(accu, 1) = coq_env; // We store the fixpoint in the first field
-	    for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
-	    Code_val(accu) = pc;
-	    sp += rec_pos;
-	    *--sp = accu;
-	      /* Construction of the atom */
-	    Alloc_small(accu, 2, ATOM_FIX_TAG);
-	    Field(accu,1) = sp[0];
-	    Field(accu,0)  = sp[1];
-	    sp++; sp[0] = accu;
-	      /* Construction of the accumulator */
-	    num_args = coq_extra_args - rec_pos;
-	    Alloc_small(accu, 2+num_args, Accu_tag);
-	    Code_val(accu) = accumulate;
-	    Field(accu,1) = sp[0]; sp++;
-	    for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
-	    sp += num_args;
-	    pc = (code_t)(sp[0]);
-	    coq_env = sp[1];
-	    coq_extra_args = Long_val(sp[2]);
-	    sp += 3;
-	  }
-	}
-	Next;
-      }
-	
+            mlsize_t num_args, i;
+            num_args = 1 + coq_extra_args; /* arg1 + extra args */
+            Alloc_small(accu, num_args + 2, Closure_tag);
+            Field(accu, 1) = coq_env;
+            for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+            Code_val(accu) = pc - 3;
+            sp += num_args;
+            pc = (code_t)(sp[0]);
+            coq_env = sp[1];
+            coq_extra_args = Long_val(sp[2]);
+            sp += 3;
+          } else {
+            /* The recursif argument is an accumulator */
+            mlsize_t num_args, i;
+            /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
+            Alloc_small(accu, rec_pos + 2, Closure_tag);
+            Field(accu, 1) = coq_env; // We store the fixpoint in the first field
+            for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
+            Code_val(accu) = pc;
+            sp += rec_pos;
+            *--sp = accu;
+              /* Construction of the atom */
+            Alloc_small(accu, 2, ATOM_FIX_TAG);
+            Field(accu,1) = sp[0];
+            Field(accu,0)  = sp[1];
+            sp++; sp[0] = accu;
+              /* Construction of the accumulator */
+            num_args = coq_extra_args - rec_pos;
+            Alloc_small(accu, 2+num_args, Accu_tag);
+            Code_val(accu) = accumulate;
+            Field(accu,1) = sp[0]; sp++;
+            for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
+            sp += num_args;
+            pc = (code_t)(sp[0]);
+            coq_env = sp[1];
+            coq_extra_args = Long_val(sp[2]);
+            sp += 3;
+          }
+        }
+        Next;
+      }
+
       Instruct(CLOSURE) {
-	int nvars = *pc++;
-	int i;
-	print_instr("CLOSURE");
-	print_int(nvars);
-	if (nvars > 0) *--sp = accu;
-	Alloc_small(accu, 1 + nvars, Closure_tag);
-	Code_val(accu) = pc + *pc;
-	pc++;
-	for (i = 0; i < nvars; i++) {
-	  print_lint(sp[i]);
-	  Field(accu, i + 1) = sp[i];
-	}
-	sp += nvars;
-	Next;
+        int nvars = *pc++;
+        int i;
+        print_instr("CLOSURE");
+        print_int(nvars);
+        if (nvars > 0) *--sp = accu;
+        Alloc_small(accu, 1 + nvars, Closure_tag);
+        Code_val(accu) = pc + *pc;
+        pc++;
+        for (i = 0; i < nvars; i++) {
+          print_lint(sp[i]);
+          Field(accu, i + 1) = sp[i];
+        }
+        sp += nvars;
+        Next;
       }
 
       Instruct(CLOSUREREC) {
-	int nfuncs = *pc++;
-	int nvars = *pc++;
-	int start = *pc++;
-	int i;
-	value * p;
-	print_instr("CLOSUREREC");
-	if (nvars > 0) *--sp = accu;
-	/* construction du vecteur de type */
+        int nfuncs = *pc++;
+        int nvars = *pc++;
+        int start = *pc++;
+        int i;
+        value * p;
+        print_instr("CLOSUREREC");
+        if (nvars > 0) *--sp = accu;
+        /* construction du vecteur de type */
         Alloc_small(accu, nfuncs, Abstract_tag);
-	for(i = 0; i < nfuncs; i++) {
-	  Field(accu,i) = (value)(pc+pc[i]);
-	}
-	pc += nfuncs;
-	*--sp=accu;
-	Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
-	Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
-	/* On remplie la partie pour les variables libres */
-	p = &Field(accu, nfuncs * 2 - 1);
-	for (i = 0; i < nvars; i++) {
-	  *p++ = *sp++;
-	}
-	p = &Field(accu, 0);
-	*p = (value) (pc + pc[0]);
-	p++;
-	for (i = 1; i < nfuncs; i++) {
-	  *p = Make_header(i * 2, Infix_tag, Caml_white);
-	  p++;                                /* color irrelevant. */
-	  *p = (value) (pc + pc[i]);
-	  p++;
-	}
-	pc += nfuncs;
-	accu = accu + 2 * start * sizeof(value);
-	Next;
-      }
-
-      Instruct(CLOSURECOFIX){ 
-	int nfunc = *pc++;
-	int nvars = *pc++;
-	int start = *pc++;
-	int i, j , size;
-	value * p;
-	print_instr("CLOSURECOFIX");
-	if (nvars > 0) *--sp = accu;
-	/* construction du vecteur de type */
+        for(i = 0; i < nfuncs; i++) {
+          Field(accu,i) = (value)(pc+pc[i]);
+        }
+        pc += nfuncs;
+        *--sp=accu;
+        Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
+        Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
+        /* On remplie la partie pour les variables libres */
+        p = &Field(accu, nfuncs * 2 - 1);
+        for (i = 0; i < nvars; i++) {
+          *p++ = *sp++;
+        }
+        p = &Field(accu, 0);
+        *p = (value) (pc + pc[0]);
+        p++;
+        for (i = 1; i < nfuncs; i++) {
+          *p = Make_header(i * 2, Infix_tag, Caml_white);
+          p++;                                /* color irrelevant. */
+          *p = (value) (pc + pc[i]);
+          p++;
+        }
+        pc += nfuncs;
+        accu = accu + 2 * start * sizeof(value);
+        Next;
+      }
+
+      Instruct(CLOSURECOFIX){
+        int nfunc = *pc++;
+        int nvars = *pc++;
+        int start = *pc++;
+        int i, j , size;
+        value * p;
+        print_instr("CLOSURECOFIX");
+        if (nvars > 0) *--sp = accu;
+        /* construction du vecteur de type */
         Alloc_small(accu, nfunc, Abstract_tag);
-	for(i = 0; i < nfunc; i++) {
-	  Field(accu,i) = (value)(pc+pc[i]);
-	}
-	pc += nfunc;
-	*--sp=accu;
+        for(i = 0; i < nfunc; i++) {
+          Field(accu,i) = (value)(pc+pc[i]);
+        }
+        pc += nfunc;
+        *--sp=accu;
 
         /* Creation des blocks accumulate */
         for(i=0; i < nfunc; i++) {
-	  Alloc_small(accu, 2, Accu_tag);
-	  Code_val(accu) = accumulate;
-	  Field(accu,1) = Val_int(1);
-	  *--sp=accu;
-	}
-	/* creation des fonction cofix */
+          Alloc_small(accu, 2, Accu_tag);
+          Code_val(accu) = accumulate;
+          Field(accu,1) = Val_int(1);
+          *--sp=accu;
+        }
+        /* creation des fonction cofix */
 
         p = sp;
-	size = nfunc + nvars + 2;
-	for (i=0; i < nfunc; i++) {
-
-	  Alloc_small(accu, size, Closure_tag);
-	  Code_val(accu) = pc+pc[i];
-	  for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
-	  Field(accu, size - 1) = p[nfunc];
-	  for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
-	  *--sp = accu;
+        size = nfunc + nvars + 2;
+        for (i=0; i < nfunc; i++) {
+
+          Alloc_small(accu, size, Closure_tag);
+          Code_val(accu) = pc+pc[i];
+          for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
+          Field(accu, size - 1) = p[nfunc];
+          for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
+          *--sp = accu;
           /* creation du block contenant le cofix */
 
-	  Alloc_small(accu,1, ATOM_COFIX_TAG);
-	  Field(accu, 0) = sp[0];
-	  *sp = accu;
-	  /* mise a jour du block accumulate */
-	  caml_modify(&Field(p[i], 1),*sp);
-	  sp++;
-	}
-	pc += nfunc;
-	accu = p[start];
+          Alloc_small(accu,1, ATOM_COFIX_TAG);
+          Field(accu, 0) = sp[0];
+          *sp = accu;
+          /* mise a jour du block accumulate */
+          caml_modify(&Field(p[i], 1),*sp);
+          sp++;
+        }
+        pc += nfunc;
+        accu = p[start];
         sp = p + nfunc + 1 + nvars;
-	print_instr("ici4");
-	Next;
+        print_instr("ici4");
+        Next;
       }
 
-    
+
       Instruct(PUSHOFFSETCLOSURE) {
-	print_instr("PUSHOFFSETCLOSURE");
-	*--sp = accu;
+        print_instr("PUSHOFFSETCLOSURE");
+        *--sp = accu;
       } /* fallthrough */
       Instruct(OFFSETCLOSURE) {
-	print_instr("OFFSETCLOSURE");
-	accu = coq_env + *pc++ * sizeof(value); Next;
+        print_instr("OFFSETCLOSURE");
+        accu = coq_env + *pc++ * sizeof(value); Next;
       }
       Instruct(PUSHOFFSETCLOSUREM2) {
-	print_instr("PUSHOFFSETCLOSUREM2");
-	*--sp = accu;
+        print_instr("PUSHOFFSETCLOSUREM2");
+        *--sp = accu;
       } /* fallthrough */
       Instruct(OFFSETCLOSUREM2) {
-	print_instr("OFFSETCLOSUREM2");
-	accu = coq_env - 2 * sizeof(value); Next;
+        print_instr("OFFSETCLOSUREM2");
+        accu = coq_env - 2 * sizeof(value); Next;
       }
       Instruct(PUSHOFFSETCLOSURE0) {
-	print_instr("PUSHOFFSETCLOSURE0");
-	*--sp = accu; 
+        print_instr("PUSHOFFSETCLOSURE0");
+        *--sp = accu;
       }/* fallthrough */
       Instruct(OFFSETCLOSURE0) {
-	print_instr("OFFSETCLOSURE0");
-	accu = coq_env; Next;
+        print_instr("OFFSETCLOSURE0");
+        accu = coq_env; Next;
       }
       Instruct(PUSHOFFSETCLOSURE2){
-	print_instr("PUSHOFFSETCLOSURE2");
-	*--sp = accu; /* fallthrough */
+        print_instr("PUSHOFFSETCLOSURE2");
+        *--sp = accu; /* fallthrough */
       }
       Instruct(OFFSETCLOSURE2) {
-	print_instr("OFFSETCLOSURE2");
-	accu = coq_env + 2 * sizeof(value); Next;
+        print_instr("OFFSETCLOSURE2");
+        accu = coq_env + 2 * sizeof(value); Next;
       }
 
 /* Access to global variables */
 
       Instruct(PUSHGETGLOBAL) {
-	print_instr("PUSH");
-	*--sp = accu;
+        print_instr("PUSH");
+        *--sp = accu;
       }
       /* Fallthrough */
       Instruct(GETGLOBAL){
-	print_instr("GETGLOBAL");
-	print_int(*pc);
-	accu = Field(coq_global_data, *pc);
+        print_instr("GETGLOBAL");
+        print_int(*pc);
+        accu = Field(coq_global_data, *pc);
         pc++;
         Next;
-      }    
+      }
 
 /* Allocation of blocks */
 
       Instruct(MAKEBLOCK) {
-	mlsize_t wosize = *pc++;
-	tag_t tag = *pc++;
-	mlsize_t i;
-	value block;
-	print_instr("MAKEBLOCK, tag=");
-	Alloc_small(block, wosize, tag);
-	Field(block, 0) = accu;
-	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
-	accu = block;
-	Next;
+        mlsize_t wosize = *pc++;
+        tag_t tag = *pc++;
+        mlsize_t i;
+        value block;
+        print_instr("MAKEBLOCK, tag=");
+        Alloc_small(block, wosize, tag);
+        Field(block, 0) = accu;
+        for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
+        accu = block;
+        Next;
       }
       Instruct(MAKEBLOCK1) {
-	
-	tag_t tag = *pc++;
-	value block;
-	print_instr("MAKEBLOCK1, tag=");
-	print_int(tag);
-	Alloc_small(block, 1, tag);
-	Field(block, 0) = accu;
-	accu = block;
-	Next;
+
+        tag_t tag = *pc++;
+        value block;
+        print_instr("MAKEBLOCK1, tag=");
+        print_int(tag);
+        Alloc_small(block, 1, tag);
+        Field(block, 0) = accu;
+        accu = block;
+        Next;
       }
       Instruct(MAKEBLOCK2) {
-	
-	tag_t tag = *pc++;
-	value block;
-	print_instr("MAKEBLOCK2, tag=");
-	print_int(tag);
-	Alloc_small(block, 2, tag);
-	Field(block, 0) = accu;
-	Field(block, 1) = sp[0];
-	sp += 1;
-	accu = block;
-	Next;
+
+        tag_t tag = *pc++;
+        value block;
+        print_instr("MAKEBLOCK2, tag=");
+        print_int(tag);
+        Alloc_small(block, 2, tag);
+        Field(block, 0) = accu;
+        Field(block, 1) = sp[0];
+        sp += 1;
+        accu = block;
+        Next;
       }
       Instruct(MAKEBLOCK3) {
-	tag_t tag = *pc++;
-	value block;
-	print_instr("MAKEBLOCK3, tag=");
-	print_int(tag);
-	Alloc_small(block, 3, tag);
-	Field(block, 0) = accu;
-	Field(block, 1) = sp[0];
-	Field(block, 2) = sp[1];
-	sp += 2;
-	accu = block;
-	Next;
+        tag_t tag = *pc++;
+        value block;
+        print_instr("MAKEBLOCK3, tag=");
+        print_int(tag);
+        Alloc_small(block, 3, tag);
+        Field(block, 0) = accu;
+        Field(block, 1) = sp[0];
+        Field(block, 2) = sp[1];
+        sp += 2;
+        accu = block;
+        Next;
       }
       Instruct(MAKEBLOCK4) {
-	tag_t tag = *pc++;
-	value block;
-	print_instr("MAKEBLOCK4, tag=");
-	print_int(tag);
-	Alloc_small(block, 4, tag);
-	Field(block, 0) = accu;
-	Field(block, 1) = sp[0];
-	Field(block, 2) = sp[1];
-	Field(block, 3) = sp[2];
-	sp += 3;
-	accu = block;
-	Next;
-      }
-
-  
+        tag_t tag = *pc++;
+        value block;
+        print_instr("MAKEBLOCK4, tag=");
+        print_int(tag);
+        Alloc_small(block, 4, tag);
+        Field(block, 0) = accu;
+        Field(block, 1) = sp[0];
+        Field(block, 2) = sp[1];
+        Field(block, 3) = sp[2];
+        sp += 3;
+        accu = block;
+        Next;
+      }
+
+
 /* Access to components of blocks */
-        
+
       Instruct(SWITCH) {
-	uint32_t sizes = *pc++;
-	print_instr("SWITCH");
-	print_int(sizes & 0xFFFFFF);
-	if (Is_block(accu)) {
-	  long index = Tag_val(accu);
-	  print_instr("block");
-	  print_lint(index);
-	  pc += pc[(sizes & 0xFFFFFF) + index];
-	} else {
-	  long index = Long_val(accu);
-	  print_instr("constant");
-	  print_lint(index);
-	  pc += pc[index];
-	}
-	  Next;
+        uint32_t sizes = *pc++;
+        print_instr("SWITCH");
+        print_int(sizes & 0xFFFFFF);
+        if (Is_block(accu)) {
+          long index = Tag_val(accu);
+          print_instr("block");
+          print_lint(index);
+          pc += pc[(sizes & 0xFFFFFF) + index];
+        } else {
+          long index = Long_val(accu);
+          print_instr("constant");
+          print_lint(index);
+          pc += pc[index];
+        }
+          Next;
       }
 
       Instruct(PUSHFIELDS){
-	int i;
-	int size = *pc++;
-	print_instr("PUSHFIELDS");
-	sp -= size;
-	for(i=0;i<size;i++)sp[i] = Field(accu,i);
-	Next;
-      }
-      
+        int i;
+        int size = *pc++;
+        print_instr("PUSHFIELDS");
+        sp -= size;
+        for(i=0;i<size;i++)sp[i] = Field(accu,i);
+        Next;
+      }
+
       Instruct(GETFIELD0){
-	print_instr("GETFIELD0");
-	accu = Field(accu, 0); 
-	Next;
+        print_instr("GETFIELD0");
+        accu = Field(accu, 0);
+        Next;
       }
 
       Instruct(GETFIELD1){
-	print_instr("GETFIELD1");
-	accu = Field(accu, 1);
-	Next;
+        print_instr("GETFIELD1");
+        accu = Field(accu, 1);
+        Next;
       }
 
       Instruct(GETFIELD){
-	print_instr("GETFIELD");
-	accu = Field(accu, *pc); 
-	pc++; 
-	Next;
+        print_instr("GETFIELD");
+        accu = Field(accu, *pc);
+        pc++;
+        Next;
       }
-      
+
       Instruct(SETFIELD0){
-	print_instr("SETFIELD0");
-	caml_modify(&Field(accu, 0),*sp);
-	sp++;
-	Next;
+        print_instr("SETFIELD0");
+        caml_modify(&Field(accu, 0),*sp);
+        sp++;
+        Next;
       }
-	
+
       Instruct(SETFIELD1){
-	print_instr("SETFIELD1");
-	caml_modify(&Field(accu, 1),*sp);
-       	sp++;
-	Next; 
+        print_instr("SETFIELD1");
+        caml_modify(&Field(accu, 1),*sp);
+        sp++;
+        Next;
       }
-       
+
       Instruct(SETFIELD){
-	print_instr("SETFIELD");
-	caml_modify(&Field(accu, *pc),*sp);
-	sp++; pc++;
-	Next;
+        print_instr("SETFIELD");
+        caml_modify(&Field(accu, *pc),*sp);
+        sp++; pc++;
+        Next;
       }
 
 
       Instruct(PROJ){
         do_proj:
-	print_instr("PROJ");
-	if (Is_accu (accu)) {
+        print_instr("PROJ");
+        if (Is_accu (accu)) {
           *--sp = accu; // Save matched block on stack
           accu = Field(accu, 1); // Save atom to accu register
           switch (Tag_val(accu)) {
@@ -1023,135 +1023,135 @@ value coq_interprete
               accu = block;
             }
           }
-	} else {
+        } else {
           accu = Field(accu, *pc);
           pc += 2;
-	}
-	Next;
+        }
+        Next;
       }
 
 /* Integer constants */
 
       Instruct(CONST0){
-	print_instr("CONST0");
-	accu = Val_int(0); Next;}
+        print_instr("CONST0");
+        accu = Val_int(0); Next;}
       Instruct(CONST1){
-	print_instr("CONST1");
-	accu = Val_int(1); Next;}
+        print_instr("CONST1");
+        accu = Val_int(1); Next;}
       Instruct(CONST2){
-	print_instr("CONST2");
-	accu = Val_int(2); Next;}
+        print_instr("CONST2");
+        accu = Val_int(2); Next;}
       Instruct(CONST3){
-	print_instr("CONST3");
-	accu = Val_int(3); Next;}
-      
+        print_instr("CONST3");
+        accu = Val_int(3); Next;}
+
       Instruct(PUSHCONST0){
-	print_instr("PUSHCONST0");
-	*--sp = accu; accu = Val_int(0); Next;
+        print_instr("PUSHCONST0");
+        *--sp = accu; accu = Val_int(0); Next;
       }
       Instruct(PUSHCONST1){
-	print_instr("PUSHCONST1");
-	*--sp = accu; accu = Val_int(1); Next;
+        print_instr("PUSHCONST1");
+        *--sp = accu; accu = Val_int(1); Next;
       }
       Instruct(PUSHCONST2){
-	print_instr("PUSHCONST2");
-	*--sp = accu; accu = Val_int(2); Next;
+        print_instr("PUSHCONST2");
+        *--sp = accu; accu = Val_int(2); Next;
       }
       Instruct(PUSHCONST3){
-	print_instr("PUSHCONST3");
-	*--sp = accu; accu = Val_int(3); Next;
+        print_instr("PUSHCONST3");
+        *--sp = accu; accu = Val_int(3); Next;
       }
 
       Instruct(PUSHCONSTINT){
-	print_instr("PUSHCONSTINT");
-	*--sp = accu;
+        print_instr("PUSHCONSTINT");
+        *--sp = accu;
       }
       /* Fallthrough */
       Instruct(CONSTINT) {
-	print_instr("CONSTINT");
-	print_int(*pc);
-	accu = Val_int(*pc);
-	pc++;
-	Next;
+        print_instr("CONSTINT");
+        print_int(*pc);
+        accu = Val_int(*pc);
+        pc++;
+        Next;
       }
 
       /* Special operations for reduction of open term */
       Instruct(ACCUMULATE) {
-	mlsize_t i, size;
-	print_instr("ACCUMULATE");
-	size = Wosize_val(coq_env);
-	Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
-	for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
-	for(i = size; i <= coq_extra_args + size; i++) 
-	  Field(accu, i) = *sp++;
-	pc = (code_t)(sp[0]);
-	coq_env = sp[1];
-	coq_extra_args = Long_val(sp[2]);
-	sp += 3;
-	Next;
-      }  
+        mlsize_t i, size;
+        print_instr("ACCUMULATE");
+        size = Wosize_val(coq_env);
+        Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+        for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
+        for(i = size; i <= coq_extra_args + size; i++)
+          Field(accu, i) = *sp++;
+        pc = (code_t)(sp[0]);
+        coq_env = sp[1];
+        coq_extra_args = Long_val(sp[2]);
+        sp += 3;
+        Next;
+      }
       Instruct(MAKESWITCHBLOCK) {
-	print_instr("MAKESWITCHBLOCK");
-	*--sp = accu; // Save matched block on stack
-	accu = Field(accu,1); // Save atom to accu register
-	switch (Tag_val(accu)) {
-	case ATOM_COFIX_TAG: // We are forcing a cofix
-	  {
-	    mlsize_t i, nargs;
-	    print_instr("COFIX_TAG");
-	    sp-=2;
-	    pc++;
+        print_instr("MAKESWITCHBLOCK");
+        *--sp = accu; // Save matched block on stack
+        accu = Field(accu,1); // Save atom to accu register
+        switch (Tag_val(accu)) {
+        case ATOM_COFIX_TAG: // We are forcing a cofix
+          {
+            mlsize_t i, nargs;
+            print_instr("COFIX_TAG");
+            sp-=2;
+            pc++;
             // Push the return address
-	    sp[0] = (value) (pc + *pc);
-	    sp[1] = coq_env;
-	    coq_env = Field(accu,0); // Pointer to suspension
-	    accu = sp[2]; // Save accumulator to accu register
-	    sp[2] = Val_long(coq_extra_args); // Push number of args for return
-	    nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+            sp[0] = (value) (pc + *pc);
+            sp[1] = coq_env;
+            coq_env = Field(accu,0); // Pointer to suspension
+            accu = sp[2]; // Save accumulator to accu register
+            sp[2] = Val_long(coq_extra_args); // Push number of args for return
+            nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
             // Push arguments to stack
             CHECK_STACK(nargs+1);
-	    sp -= nargs;
-	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); 
+            sp -= nargs;
+            for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
             *--sp = accu; // Leftmost argument is the pointer to the suspension
-	    print_lint(nargs);
-	    coq_extra_args = nargs;
-	    pc = Code_val(coq_env); // Trigger evaluation
-	    goto check_stack;
-	  }
-	case ATOM_COFIXEVALUATED_TAG: 
-	  {
-	    print_instr("COFIX_EVAL_TAG");
-	    accu = Field(accu,1);
-	    pc++;
-	    pc = pc + *pc;
-	    sp++;
-	    Next;
-	  }
-	default: 
-	  {  
-	    mlsize_t sz;
-	    int i, annot;
-	    code_t typlbl,swlbl;
-	    print_instr("MAKESWITCHBLOCK");
-	    
-	    typlbl = (code_t)pc + *pc; 
-	    pc++;
-	    swlbl = (code_t)pc + *pc; 
-	    pc++;
-	    annot = *pc++;
-	    sz = *pc++;
-	    *--sp=Field(coq_global_data, annot);
-	    /* We save the stack */
-	    if (sz == 0) accu = Atom(0);
-	    else {
-	      Alloc_small(accu, sz, Default_tag);
-	      if (Field(*sp, 2) == Val_true) {
-		for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
-	      }else{
-		for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
-	      }
-	    }
-	    *--sp = accu;
+            print_lint(nargs);
+            coq_extra_args = nargs;
+            pc = Code_val(coq_env); // Trigger evaluation
+            goto check_stack;
+          }
+        case ATOM_COFIXEVALUATED_TAG:
+          {
+            print_instr("COFIX_EVAL_TAG");
+            accu = Field(accu,1);
+            pc++;
+            pc = pc + *pc;
+            sp++;
+            Next;
+          }
+        default:
+          {
+            mlsize_t sz;
+            int i, annot;
+            code_t typlbl,swlbl;
+            print_instr("MAKESWITCHBLOCK");
+
+            typlbl = (code_t)pc + *pc;
+            pc++;
+            swlbl = (code_t)pc + *pc;
+            pc++;
+            annot = *pc++;
+            sz = *pc++;
+            *--sp=Field(coq_global_data, annot);
+            /* We save the stack */
+            if (sz == 0) accu = Atom(0);
+            else {
+              Alloc_small(accu, sz, Default_tag);
+              if (Field(*sp, 2) == Val_true) {
+                for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
+              }else{
+                for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
+              }
+            }
+            *--sp = accu;
             /* Create bytecode wrappers */
             Alloc_small(accu, 1, Abstract_tag);
             Code_val(accu) = typlbl;
@@ -1168,47 +1168,47 @@ value coq_interprete
             Field(accu, 4) = coq_env;
             sp += 3;
             sp[0] = accu;
-	    /* We create the atom */
-	    Alloc_small(accu, 2, ATOM_SWITCH_TAG);
-	    Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
-	    sp++;sp[0] = accu;
-	    /* We create the accumulator */
-	    Alloc_small(accu, 2, Accu_tag);
-	    Code_val(accu) = accumulate; 
-	    Field(accu,1) = *sp++;
-	  }
-	}
-	Next;
-      }
-
-	
-         
+            /* We create the atom */
+            Alloc_small(accu, 2, ATOM_SWITCH_TAG);
+            Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
+            sp++;sp[0] = accu;
+            /* We create the accumulator */
+            Alloc_small(accu, 2, Accu_tag);
+            Code_val(accu) = accumulate;
+            Field(accu,1) = *sp++;
+          }
+        }
+        Next;
+      }
+
+
+
       Instruct(MAKEACCU) {
-	int i;
-	print_instr("MAKEACCU");
-	Alloc_small(accu, coq_extra_args + 3, Accu_tag);
-	Code_val(accu) = accumulate;
-	Field(accu,1) = Field(coq_atom_tbl, *pc);
-	for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
-	pc = (code_t)(sp[0]);
-	coq_env = sp[1];
-	coq_extra_args = Long_val(sp[2]);
-	sp += 3;
-	Next;
-      }
-     
+        int i;
+        print_instr("MAKEACCU");
+        Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+        Code_val(accu) = accumulate;
+        Field(accu,1) = Field(coq_atom_tbl, *pc);
+        for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+        pc = (code_t)(sp[0]);
+        coq_env = sp[1];
+        coq_extra_args = Long_val(sp[2]);
+        sp += 3;
+        Next;
+      }
+
       Instruct(MAKEPROD) {
-	print_instr("MAKEPROD");
-	*--sp=accu;
-	Alloc_small(accu,2,0);
-	Field(accu, 0) = sp[0];
-	Field(accu, 1) = sp[1];
-	sp += 2;
-	Next;
+        print_instr("MAKEPROD");
+        *--sp=accu;
+        Alloc_small(accu,2,0);
+        Field(accu, 0) = sp[0];
+        Field(accu, 1) = sp[1];
+        sp += 2;
+        Next;
       }
 
       Instruct(BRANCH) {
-	/* unconditional branching */
+        /* unconditional branching */
         print_instr("BRANCH");
         pc += *pc;
         /* pc = (code_t)(pc+*pc); */
@@ -1220,7 +1220,7 @@ value coq_interprete
         CheckInt2();
       }
       Instruct(ADDINT63) {
-        /* Adds the integer in the accumulator with 
+        /* Adds the integer in the accumulator with
            the one ontop of the stack (which is poped)*/
         print_instr("ADDINT63");
         Uint63_add(accu, *sp++);
@@ -1230,27 +1230,27 @@ value coq_interprete
       Instruct (CHECKADDCINT63) {
         print_instr("CHECKADDCINT63");
         CheckInt2();
-	/* returns the sum with a carry */
+        /* returns the sum with a carry */
         int c;
         Uint63_add(accu, *sp);
         Uint63_lt(c, accu, *sp);
         Swap_accu_sp;
         AllocCarry(c);
         Field(accu, 0) = *sp++;
-	Next;
+        Next;
       }
 
       Instruct (CHECKADDCARRYCINT63) {
         print_instr("ADDCARRYCINT63");
         CheckInt2();
-	/* returns the sum plus one with a carry */
+        /* returns the sum plus one with a carry */
         int c;
         Uint63_addcarry(accu, *sp);
         Uint63_leq(c, accu, *sp);
         Swap_accu_sp;
         AllocCarry(c);
         Field(accu, 0) = *sp++;
-	Next;
+        Next;
       }
 
       Instruct (CHECKSUBINT63) {
@@ -1259,7 +1259,7 @@ value coq_interprete
       }
       Instruct (SUBINT63) {
         print_instr("SUBINT63");
-	/* returns the subtraction */
+        /* returns the subtraction */
         Uint63_sub(accu, *sp++);
         Next;
       }
@@ -1267,35 +1267,35 @@ value coq_interprete
       Instruct (CHECKSUBCINT63) {
         print_instr("SUBCINT63");
         CheckInt2();
-	/* returns the subtraction with a carry */
+        /* returns the subtraction with a carry */
         int c;
         Uint63_lt(c, accu, *sp);
         Uint63_sub(accu, *sp);
         Swap_accu_sp;
         AllocCarry(c);
         Field(accu, 0) = *sp++;
-	Next;
+        Next;
       }
 
       Instruct (CHECKSUBCARRYCINT63) {
         print_instr("SUBCARRYCINT63");
         CheckInt2();
-	/* returns the subtraction minus one with a carry */
+        /* returns the subtraction minus one with a carry */
         int c;
         Uint63_leq(c,accu,*sp);
         Uint63_subcarry(accu,*sp);
         Swap_accu_sp;
         AllocCarry(c);
         Field(accu, 0) = *sp++;
-	Next;
+        Next;
       }
 
       Instruct (CHECKMULINT63) {
         print_instr("MULINT63");
         CheckInt2();
-	/* returns the multiplication */
+        /* returns the multiplication */
         Uint63_mul(accu,*sp++);
-	Next;
+        Next;
       }
 
       Instruct (CHECKMULCINT63) {
@@ -1320,11 +1320,11 @@ value coq_interprete
         Uint63_eq0(b, *sp);
         if (b) {
           accu = *sp++;
-	}
-	else {
+        }
+        else {
           Uint63_div(accu, *sp++);
         }
-	Next;
+        Next;
       }
 
       Instruct(CHECKMODINT63) {
@@ -1334,11 +1334,11 @@ value coq_interprete
         Uint63_eq0(b, *sp);
         if (b) {
           accu = *sp++;
-	}
+        }
         else {
           Uint63_mod(accu,*sp++);
-	}
-	Next;
+        }
+        Next;
       }
 
       Instruct (CHECKDIVEUCLINT63) {
@@ -1366,7 +1366,7 @@ value coq_interprete
           Field(accu, 1) = sp[0];
           sp += 2;
         }
-	Next;
+        Next;
       }
 
       Instruct (CHECKDIV21INT63) {
@@ -1520,14 +1520,14 @@ value coq_interprete
       Instruct (ISINT){
         print_instr("ISINT");
         accu = (Is_uint63(accu)) ? coq_true : coq_false;
-	Next;
+        Next;
       }
 
       Instruct (AREINT2){
         print_instr("AREINT2");
         accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
         sp++;
-	Next;
+        Next;
       }
 
 
@@ -1734,12 +1734,12 @@ value coq_interprete
 /* Debugging and machine control */
 
       Instruct(STOP){
-	print_instr("STOP");
-	coq_sp = sp;
+        print_instr("STOP");
+        coq_sp = sp;
         CAMLreturn(accu);
       }
-      
-  
+
+
 #ifndef THREADED_CODE
     default:
       /*fprintf(stderr, "%d\n", *pc);*/
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index a1c49bee95..91d6773b1f 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -9,7 +9,7 @@
 /***********************************************************************/
 
 #include <stdio.h>
-#include <string.h> 
+#include <string.h>
 #include <caml/alloc.h>
 #include <caml/address_class.h>
 #include "coq_gc.h"
@@ -31,7 +31,7 @@ int drawinstr;
 
 long coq_saved_sp_offset;
 value * coq_sp;
-/* Some predefined pointer code */ 
+/* Some predefined pointer code */
 code_t accumulate;
 
 /* functions over global environment */
@@ -80,7 +80,7 @@ void init_coq_stack()
   coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value);
   coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
   coq_max_stack_size = Coq_max_stack_size;
-}  
+}
 
 void init_coq_interpreter()
 {
@@ -96,14 +96,14 @@ value init_coq_vm(value unit) /* ML */
     fprintf(stderr,"already open \n");fflush(stderr);}
   else {
     drawinstr=0;
-#ifdef THREADED_CODE   
+#ifdef THREADED_CODE
     init_arity();
 #endif /* THREADED_CODE */
     /* Allocate the table of global and the stack */
     init_coq_stack();
     /* Initialing the interpreter */
     init_coq_interpreter();
-    
+
     /* Some predefined pointer code.
      * It is typically contained in accumulator blocks whose tag is 0 and thus
      * scanned by the GC, so make it look like an OCaml block. */
@@ -117,7 +117,7 @@ value init_coq_vm(value unit) /* ML */
       coq_prev_scan_roots_hook = scan_roots_hook;
     scan_roots_hook = coq_scan_roots;
     coq_vm_initialized = 1;
-  } 
+  }
   return Val_unit;;
 }
 
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 1ea461c5e5..7f982d0477 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -39,7 +39,7 @@ extern int drawinstr;
 /* interp state */
 
 extern value * coq_sp;
-/* Some predefined pointer code */ 
+/* Some predefined pointer code */
 extern code_t accumulate;
 
 /* functions over global environment */
@@ -49,7 +49,7 @@ value coq_static_alloc(value size);  /* ML */
 value init_coq_vm(value unit); /* ML */
 value re_init_coq_vm(value unit); /* ML */
 
-void  realloc_coq_stack(asize_t required_space); 
+void  realloc_coq_stack(asize_t required_space);
 value coq_set_transp_value(value transp); /* ML */
 value get_coq_transp_value(value unit); /* ML */
 #endif /* _COQ_MEMORY_ */
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);
     }