Merge branch 'v8.6'

5 files changed, 14 insertions, 8 deletions

diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 8c5ab0ecb..885594ac7 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -14,6 +14,8 @@
 /* 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,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index df5fdce75..ddf40e2eb 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -539,6 +539,7 @@ value coq_interprete
 	  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); 
@@ -553,10 +554,10 @@ value coq_interprete
 	  } else {
 	    /* The recursif argument is an accumulator */
 	    mlsize_t num_args, i;
-	    /* Construction of partially applied PF */
+	    /* Construction of fixpoint applied to its [rec_pos-1] first arguments */
 	    Alloc_small(accu, rec_pos + 2, Closure_tag); 
-	    Field(accu, 1) = coq_env;
-	    for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i];
+	    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;
@@ -1024,7 +1025,7 @@ value coq_interprete
 	    annot = *pc++;
 	    sz = *pc++;
 	    *--sp=Field(coq_global_data, annot);
-	    /* On sauve la pile */
+	    /* We save the stack */
 	    if (sz == 0) accu = Atom(0);
 	    else {
 	      Alloc_small(accu, sz, Default_tag);
@@ -1035,17 +1036,17 @@ value coq_interprete
 	      }
 	    }
 	    *--sp = accu;
-	    /* On cree le zipper switch */
+	    /* We create the switch zipper */
 	    Alloc_small(accu, 5, Default_tag);
 	    Field(accu, 0) =  (value)typlbl; Field(accu, 1) = (value)swlbl; 
 	    Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; 
 	    Field(accu, 4) = coq_env;
 	    sp++;sp[0] = accu;
-	    /* On cree l'atome */
+	    /* 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;
-	    /* On cree l'accumulateur */
+	    /* We create the accumulator */
 	    Alloc_small(accu, 2, Accu_tag);
 	    Code_val(accu) = accumulate; 
 	    Field(accu,1) = *sp++;
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 52f0730f3..2fe917eca 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -506,6 +506,7 @@ let comp_args comp_expr reloc args sz cont =
   done;
   !c
 
+(* Precondition: args not empty *)
 let comp_app comp_fun comp_arg reloc f args sz cont =
   let nargs = Array.length args in
   match is_tailcall cont with
diff --git a/kernel/make-opcodes b/kernel/make-opcodes
index c8f573c68..e1371b3d0 100644
--- a/kernel/make-opcodes
+++ b/kernel/make-opcodes
@@ -1,2 +1,3 @@
 $1=="enum" {n=0; next; }
-           {for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}}
+           {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n");
+           for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}}
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 894f5296a..74d956bef 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -77,6 +77,7 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
+     (* on the fly eta expansion *)
       conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
   | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _