Merge branch 'v8.6'

2 files changed, 50 insertions, 16 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 5dec3b785c..af89712d5e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -891,25 +891,58 @@ value coq_interprete
 
 
       Instruct(PROJ){
+        do_proj:
 	print_instr("PROJ");
 	if (Is_accu (accu)) {
-          value block;
-	  /* Skip over the index of projected field */
-	  pc++;
-	  /* Create atom */
-	  Alloc_small(block, 2, ATOM_PROJ_TAG);
-	  Field(block, 0) = Field(coq_global_data, *pc);
-	  Field(block, 1) = accu;
-          accu = block;
-          /* Create accumulator */
-          Alloc_small(block, 2, Accu_tag);
-          Code_val(block) = accumulate;
-          Field(block, 1) = accu;
-          accu = block;
+          *--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;
+              sp -= 2;
+              // Push the current instruction as the return address
+              sp[0] = (value)(pc - 1);
+              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 = accu; // Last argument is the pointer to the suspension
+              coq_extra_args = nargs;
+              pc = Code_val(coq_env); // Trigger evaluation
+              goto check_stack;
+            }
+          case ATOM_COFIXEVALUATED_TAG:
+            {
+              accu = Field(accu, 1);
+              ++sp;
+              goto do_proj;
+            }
+          default:
+            {
+              value block;
+              /* Skip over the index of projected field */
+              ++pc;
+              /* Create atom */
+              Alloc_small(accu, 2, ATOM_PROJ_TAG);
+              Field(accu, 0) = Field(coq_global_data, *pc++);
+              Field(accu, 1) = *sp++;
+              /* Create accumulator */
+              Alloc_small(block, 2, Accu_tag);
+              Code_val(block) = accumulate;
+              Field(block, 1) = accu;
+              accu = block;
+            }
+          }
 	} else {
-	    accu = Field(accu, *pc++);
+          accu = Field(accu, *pc);
+          pc += 2;
 	}
-	pc++;
 	Next;
       }
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 72de2f1a61..d14a254d32 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -157,7 +157,8 @@ let map_named_val f ctxt =
     (accu, d')
   in
   let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
-  { env_named_ctx = ctx; env_named_map = map }
+  if map == ctxt.env_named_map then ctxt
+  else { env_named_ctx = ctx; env_named_map = map }
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);