From 478db417e1a3a493870f012495bbc7348581ac17 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 12 Apr 2019 15:23:57 +0200
Subject: Remove `constr_of_global_in_context`

This function seems unused.
---
 kernel/typeops.ml  | 22 ----------------------
 kernel/typeops.mli |  8 --------
 2 files changed, 30 deletions(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 12ffbf4357..af710e7822 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -462,28 +462,6 @@ let type_of_global_in_context env r =
     let inst = Univ.make_abstract_instance univs in
     Inductive.type_of_constructor (cstr,inst) specif, univs
 
-(* Build a fresh instance for a given context, its associated substitution and
-   the instantiated constraints. *)
-
-let constr_of_global_in_context env r =
-  let open GlobRef in
-  match r with
-  | VarRef id -> mkVar id, Univ.AUContext.empty
-  | ConstRef c ->
-    let cb = lookup_constant c env in
-    let univs = Declareops.constant_polymorphic_context cb in
-    mkConstU (c, Univ.make_abstract_instance univs), univs
-  | IndRef ind ->
-    let (mib,_) = Inductive.lookup_mind_specif env ind in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    mkIndU (ind, Univ.make_abstract_instance univs), univs
-  | ConstructRef cstr ->
-    let (mib,_) =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
-    in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
-
 (************************************************************************)
 (************************************************************************)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cc1885f42d..c8f3e506e6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -107,14 +107,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
     usage. For non-universe-polymorphic constants, it does not
     matter. *)
 
-(** {6 Building a term from a global reference *)
-
-(** Map a global reference to a term in its local universe
-    context. The term should not be used without pushing it's universe
-    context in the environmnent of usage. For non-universe-polymorphic
-    constants, it does not matter. *)
-val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
-
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-- 
cgit v1.2.3


From d2bbd834841ba3c8b2b482a02489bd4fac19f0fb Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 4 Apr 2019 11:07:14 +0200
Subject: [vm] x86_64 registers

Backport
https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376
from OCaml VM
---
 kernel/byterun/coq_interp.c | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 2293ae9dfd..e838519fe4 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -159,6 +159,11 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define ACCU_REG asm("38")
 #define JUMPTBL_BASE_REG asm("39")
 #endif
+#ifdef __x86_64__
+#define PC_REG asm("%r15")
+#define SP_REG asm("%r14")
+#define ACCU_REG asm("%r13")
+#endif
 #endif
 
 #define CheckInt1() do{                            \
-- 
cgit v1.2.3


From d1905fbcde5905de640657a820e531929e23dd8a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:35:10 +0200
Subject: [vm] Arm 64 registers

Backport
https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f
from OCaml VM
---
 kernel/byterun/coq_interp.c | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index e838519fe4..1925ef5932 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -164,6 +164,12 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define SP_REG asm("%r14")
 #define ACCU_REG asm("%r13")
 #endif
+#ifdef __aarch64__
+#define PC_REG asm("%x19")
+#define SP_REG asm("%x20")
+#define ACCU_REG asm("%x21")
+#define JUMPTBL_BASE_REG asm("%x22")
+#endif
 #endif
 
 #define CheckInt1() do{                            \
-- 
cgit v1.2.3


From 46896e9442e74cb78ad7396054cee76564f78ec3 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:37:03 +0200
Subject: [vm] ARM registers

Backport
https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928
from OCaml VM
---
 kernel/byterun/coq_interp.c | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 1925ef5932..9742768c5d 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -148,8 +148,9 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define SP_REG asm("a4")
 #define ACCU_REG asm("d7")
 #endif
-#if defined(__arm__) && !defined(__thumb2__)
-#define PC_REG asm("r9")
+/* OCaml PR#4953: these specific registers not available in Thumb mode */
+#if defined(__arm__) && !defined(__thumb__)
+#define PC_REG asm("r6")
 #define SP_REG asm("r8")
 #define ACCU_REG asm("r7")
 #endif
-- 
cgit v1.2.3


From df6328178a92d7a51e2a08acbec5013d080e73aa Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:44:08 +0200
Subject: [vm] PPC64 registers

Backport
https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785
from OCaml VM
---
 kernel/byterun/coq_interp.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 9742768c5d..a8fd2fbe47 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -133,7 +133,7 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define SP_REG asm("%edi")
 #define ACCU_REG
 #endif
-#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#if defined(__ppc__) || defined(__ppc64__)
 #define PC_REG asm("26")
 #define SP_REG asm("27")
 #define ACCU_REG asm("28")
-- 
cgit v1.2.3


From e9fec7c112a7792d67949ef5abe3de8a8832beda Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:49:53 +0200
Subject: [vm] Backport from OCaml

Backport
https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6
and
https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e
from OCaml VM
---
 kernel/byterun/coq_interp.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a8fd2fbe47..da152599ce 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -104,7 +104,8 @@ if (sp - num_args < coq_stack_threshold) {                                     \
    several architectures.
 */
 
-#if defined(__GNUC__) && !defined(DEBUG)
+#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \
+    && !defined(__llvm__)
 #ifdef __mips__
 #define PC_REG asm("$16")
 #define SP_REG asm("$17")
-- 
cgit v1.2.3


From 016ed06128372e7b767efd4d3e1f71df9ca1e3d4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Apr 2019 10:32:39 +0200
Subject: Add union in Map interface

---
 kernel/univ.ml  | 17 +++++++----------
 kernel/univ.mli |  4 ++--
 2 files changed, 9 insertions(+), 12 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8263c68bf5..b1bbc25fe6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -231,18 +231,15 @@ module LMap = struct
   module M = HMap.Make (Level)
   include M
 
-  let union l r = 
-    merge (fun _k l r ->
-      match l, r with
-      | Some _, _ -> l
-      | _, _ -> r) l r
+  let lunion l r =
+    union (fun _k l _r -> Some l) l r
 
-  let subst_union l r = 
-    merge (fun _k l r ->
+  let subst_union l r =
+    union (fun _k l r ->
       match l, r with
-      | Some (Some _), _ -> l
-      | Some None, None -> l
-      | _, _ -> r) l r
+      | Some _, _ -> Some l
+      | None, None -> Some l
+      | _, _ -> Some r) l r
 
   let diff ext orig =
     fold (fun u v acc -> 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 5543c35741..db178c4bb0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -223,8 +223,8 @@ module LMap :
 sig
   include CMap.ExtS with type key = Level.t and module Set := LSet
 
-  val union : 'a t -> 'a t -> 'a t
-  (** [union x y] favors the bindings in the first map. *)
+  val lunion : 'a t -> 'a t -> 'a t
+  (** [lunion x y] favors the bindings in the first map. *)
 
   val diff : 'a t -> 'a t -> 'a t
   (** [diff x y] removes bindings from x that appear in y (whatever the value). *)
-- 
cgit v1.2.3


From dd60b4a292b870e08c23ddcb363630cbb2ed1227 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 2 May 2019 08:16:37 +0200
Subject: [primitive integers] Make div21 implems consistent with its
 specification

There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v

* comment the implementations with loop invariants to enable an easy
  pen&paper proof of correctness (note to reviewers: the one in
  uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
  (only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
  (cmp is computed at the end of the first loop rather than at the beginning,
   potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
  new specifiation of div21
* add a test
---
 kernel/byterun/coq_interp.c        | 39 ++++------------------------
 kernel/byterun/coq_uint63_native.h | 53 ++++++++++++++++++++++++++------------
 kernel/uint63.mli                  |  4 +++
 kernel/uint63_amd64.ml             | 26 ++++++++++++++-----
 kernel/uint63_x86.ml               | 25 +++++++++++++-----
 5 files changed, 82 insertions(+), 65 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 2293ae9dfd..e38d458b36 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1374,40 +1374,11 @@ value coq_interprete
       Instruct (CHECKDIV21INT63) {
         print_instr("DIV21INT63");
         CheckInt3();
-        /* spiwack: takes three int31 (the two first ones represent an
-                    int62) and performs the euclidian division of the
-                    int62 by the int31 */
-        /* TODO: implement this
-        bigint = UI64_of_value(accu);
-        bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
-        uint64 divisor;
-        divisor = UI64_of_value(*sp++);
-        Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */
-        /* if (I64_is_zero (divisor)) {
-           Field(accu, 0) = 1; */ /* 2*0+1 */
-        /* Field(accu, 1) = 1; */ /* 2*0+1 */
-        /* }
-        else {
-          uint64 quo, mod;
-          I64_udivmod(bigint, divisor, &quo, &mod);
-          Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
-          Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
-        } */
-        int b;
-        Uint63_eq0(b, sp[1]);
-        if (b) {
-          AllocPair();
-          Field(accu, 0) = sp[1];
-          Field(accu, 1) = sp[1];
-	}
-        else {
-          Uint63_div21(accu, sp[0], sp[1], sp);
-          sp[1] = sp[0];
-          Swap_accu_sp;
-          AllocPair();
-          Field(accu, 0) = sp[1];
-          Field(accu, 1) = sp[0];
-	}
+        Uint63_div21(accu, sp[0], sp[1], &(sp[1]));
+        Swap_accu_sp;
+        AllocPair();
+        Field(accu, 0) = sp[1];
+        Field(accu, 1) = sp[0];
         sp += 2;
         Next;
       }
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index d431dc1e5c..8dee0d69d3 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -109,37 +109,56 @@ value uint63_mulc(value x, value y, value* h) {
 #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
 #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
 
-value uint63_div21(value xh, value xl, value y, value* q) {
-  xh = (uint64_t)xh >> 1;
-  xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63);
-  xh = (uint64_t)xh >> 1;
+#define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF)
+/* precondition: y <> 0 */
+/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */
+static value uint63_div21_aux(value xh, value xl, value y, value* ql) {
+  xh = uint63_of_value(xh);
+  xl = uint63_of_value(xl);
+  y = uint63_of_value(y);
   uint64_t maskh = 0;
   uint64_t maskl = 1;
   uint64_t dh = 0;
-  uint64_t dl = (uint64_t)y >> 1;
+  uint64_t dl = y;
   int cmp = 1;
-  while (dh >= 0 && cmp) {
+  /* int n = 0 */
+  /* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0, d < 2^(2*63) */
+  while (!(dh >> (63 - 1)) && cmp) {
+    dh = (dh << 1) | (dl >> (63 - 1));
+    dl = (dl << 1) & maxuint63;
+    maskh = (maskh << 1) | (maskl >> (63 - 1));
+    maskl = (maskl << 1) & maxuint63;
+    /* ++n */
     cmp = lt128(dh,dl,xh,xl);
-    dh = (dh << 1) | (dl >> 63);
-    dl = dl << 1;
-    maskh = (maskh << 1) | (maskl >> 63);
-    maskl = maskl << 1;
   }
   uint64_t remh = xh;
   uint64_t reml = xl;
-  uint64_t quotient = 0;
+  /* uint64_t quotienth = 0; */
+  uint64_t quotientl = 0;
+  /* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
+     mask = floor(2^n), d = mask * y, n >= -1 */
   while (maskh | maskl) {
-    if (le128(dh,dl,remh,reml)) {
-      quotient = quotient | maskl;
-      if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;}
+    if (le128(dh,dl,remh,reml)) { /* if rem >= d, add one bit and subtract d */
+      /* quotienth = quotienth | maskh */
+      quotientl = quotientl | maskl;
+      remh = (uint63_lt(reml,dl)) ? (remh - dh - 1) : (remh - dh);
       reml = reml - dl;
     }
-    maskl = (maskl >> 1) | (maskh << 63);
+    maskl = (maskl >> 1) | ((maskh << (63 - 1)) & maxuint63);
     maskh = maskh >> 1;
-    dl = (dl >> 1) | (dh << 63);
+    dl = (dl >> 1) | ((dh << (63 - 1)) & maxuint63);
     dh = dh >> 1;
+    /* decr n */
   }
-  *q = Val_int(quotient);
+  *ql = Val_int(quotientl);
   return Val_int(reml);
 }
+value uint63_div21(value xh, value xl, value y, value* ql) {
+  if (uint63_of_value(y) == 0) {
+    *ql = Val_int(0);
+    return Val_int(0);
+  } else {
+    return uint63_div21_aux(xh, xl, y, ql);
+  }
+}
 #define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q))
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index b5f40ca804..f25f24512d 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -40,6 +40,10 @@ val rem     : t -> t -> t
       (* Specific arithmetic operations *)
 val mulc    : t -> t -> t * t
 val addmuldiv : t -> t -> t -> t
+
+(** [div21 xh xl y] returns [q % 2^63, r]
+    s.t. [xh * 2^63 + xl = q * y + r] and [r < y].
+    When [y] is [0], returns [0, 0]. *)
 val div21   : t -> t -> t -> t * t
 
       (* comparison *)
diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64.ml
index 010b594de8..2d4d685775 100644
--- a/kernel/uint63_amd64.ml
+++ b/kernel/uint63_amd64.ml
@@ -102,26 +102,35 @@ let le128 xh xl yh yl =
   lt xh yh || (xh = yh && le xl yl)
 
     (* division of two numbers by one *)
+(* precondition: y <> 0 *)
+(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
 let div21 xh xl y =
   let maskh = ref 0 in
   let maskl = ref 1 in
   let dh = ref 0 in
   let dl = ref y in
   let cmp = ref true in
-  while !dh >= 0 && !cmp do
-    cmp := lt128 !dh !dl xh xl;
+  (* n = ref 0 *)
+  (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
+  while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *)
     (* We don't use addmuldiv below to avoid checks on 1 *)
     dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1));
     dl := !dl lsl 1;
     maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1));
-    maskl := !maskl lsl 1
-  done; (* mask = 2^N, d = 2^N * d, d >= x *)
+    maskl := !maskl lsl 1;
+    (* incr n *)
+    cmp := lt128 !dh !dl xh xl;
+  done; (* mask = 2^n, d = 2^n * y, 2 * d > x *)
   let remh = ref xh in
   let reml = ref xl in
-  let quotient = ref 0 in
+  (* quotienth = ref 0 *)
+  let quotientl = ref 0 in
+  (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
+     mask = floor(2^n), d = mask * y, n >= -1 *)
   while !maskh lor !maskl <> 0 do
     if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
-      quotient := !quotient lor !maskl;
+      (* quotienth := !quotienth lor !maskh *)
+      quotientl := !quotientl lor !maskl;
       remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh;
       reml := !reml - !dl;
     end;
@@ -129,8 +138,11 @@ let div21 xh xl y =
     maskh := !maskh lsr 1;
     dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1));
     dh := !dh lsr 1;
+    (* decr n *)
   done;
-  !quotient, !reml
+  !quotientl, !reml
+
+let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y
 
      (* exact multiplication *)
 (* TODO: check that none of these additions could be a logical or *)
diff --git a/kernel/uint63_x86.ml b/kernel/uint63_x86.ml
index 461184c432..fa45c90241 100644
--- a/kernel/uint63_x86.ml
+++ b/kernel/uint63_x86.ml
@@ -94,26 +94,35 @@ let le128 xh xl yh yl =
   lt xh yh || (xh = yh && le xl yl)
 
     (* division of two numbers by one *)
+(* precondition: y <> 0 *)
+(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
 let div21 xh xl y =
   let maskh = ref zero in
   let maskl = ref one in
   let dh = ref zero in
   let dl = ref y in
   let cmp = ref true in
-  while le zero !dh && !cmp do
-    cmp := lt128 !dh !dl xh xl;
+  (* n = ref 0 *)
+  (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
+  while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do
     (* We don't use addmuldiv below to avoid checks on 1 *)
     dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1)));
     dl := l_sl !dl one;
     maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1)));
-    maskl := l_sl !maskl one
-  done; (* mask = 2^N, d = 2^N * d, d >= x *)
+    maskl := l_sl !maskl one;
+    (* incr n *)
+    cmp := lt128 !dh !dl xh xl;
+  done; (* mask = 2^n, d = 2^n * d, 2 * d > x *)
   let remh = ref xh in
   let reml = ref xl in
-  let quotient = ref zero in
+  (* quotienth = ref 0 *)
+  let quotientl = ref zero in
+  (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
+     mask = floor(2^n), d = mask * y, n >= -1 *)
   while not (Int64.equal (l_or !maskh !maskl) zero) do
     if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
-      quotient := l_or !quotient !maskl;
+      (* quotienth := !quotienth lor !maskh *)
+      quotientl := l_or !quotientl !maskl;
       remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh;
       reml := sub !reml !dl
     end;
@@ -121,9 +130,11 @@ let div21 xh xl y =
     maskh := l_sr !maskh one;
     dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1)));
     dh := l_sr !dh one
+    (* decr n *)
   done;
-  !quotient, !reml
+  !quotientl, !reml
 
+let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y
 
      (* exact multiplication *)
 let mulc x y =
-- 
cgit v1.2.3


From 09cdf7b1fad8761cdf7048bf38a468c8558eb0d5 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 2 May 2019 08:41:45 +0200
Subject: Remove now useless commented code

---
 kernel/byterun/coq_interp.c        | 15 +--------------
 kernel/byterun/coq_uint63_emul.h   |  2 ++
 kernel/byterun/coq_uint63_native.h |  1 +
 3 files changed, 4 insertions(+), 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index e38d458b36..1b348ae777 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -29,13 +29,6 @@
 #include "coq_uint63_emul.h"
 #endif
 
-/* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) (((uint32_t)(val)) >> 1)
-#define value_of_uint32(i)   ((value)((((uint32_t)(i)) << 1) | 1))
-#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo)))
-#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
-/* /spiwack */
-
 
 
 /* Registers for the abstract machine:
@@ -1298,12 +1291,6 @@ value coq_interprete
         /*returns the multiplication on a pair */
         print_instr("MULCINT63");
         CheckInt2();
-        /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
-        /* TODO: implement
-        p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
-        AllocPair(); */
-        /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
-        /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
         Uint63_mulc(accu, *sp, sp);
         *--sp = accu;
         AllocPair();
@@ -1587,7 +1574,7 @@ value coq_push_vstack(value stk, value max_stack_size) {
   print_instr("push_vstack");print_int(len);
    for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i);
   sp = coq_sp;
-  CHECK_STACK(uint32_of_value(max_stack_size));
+  CHECK_STACK(uint_of_value(max_stack_size));
   return Val_unit;
 }
 
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index d982f67566..528cc6fc1f 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -6,6 +6,8 @@
 
 #define Is_uint63(v) (Tag_val(v) == Custom_tag)
 
+#define uint_of_value(val) (((uint32_t)(val)) >> 1)
+
 # define DECLARE_NULLOP(name) \
 value uint63_##name() { \
   static value* cb = 0; \
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 8dee0d69d3..1fdafc9d8f 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -1,5 +1,6 @@
 #define Is_uint63(v) (Is_long(v))
 
+#define uint_of_value(val) (((uint64_t)(val)) >> 1)
 #define uint63_of_value(val) ((uint64_t)(val) >> 1)
 
 /* 2^63 * y + x as a value */
-- 
cgit v1.2.3


From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
---
 kernel/indtypes.ml  | 17 ++---------------
 kernel/indtypes.mli | 19 -------------------
 kernel/names.ml     |  3 ---
 kernel/names.mli    |  3 ---
 4 files changed, 2 insertions(+), 40 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 009eb3da38..bb3b0a538e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -49,20 +49,6 @@ let weaker_noccur_between env x nvars t =
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
-(* Errors related to inductive constructions *)
-type inductive_error = Type_errors.inductive_error =
-  | NonPos of env * constr * constr
-  | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * Id.t * constr * constr * int * int
-  | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of Id.t
-  | SameNamesConstructors of Id.t
-  | SameNamesOverlap of Id.t list
-  | NotAnArity of env * constr
-  | BadEntry
-  | LargeNonPropInductiveNotInType
-  | BadUnivs
-
 exception InductiveError = Type_errors.InductiveError
 
 (************************************************************************)
@@ -84,6 +70,7 @@ exception IllFormedInd of ill_formed_ind
 let mind_extract_params = decompose_prod_n_assum
 
 let explain_ind_err id ntyp env nparamsctxt c err =
+  let open Type_errors in
   let (_lparams,c') = mind_extract_params nparamsctxt c in
   match err with
     | LocalNonPos kt ->
@@ -329,7 +316,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
 	      if not recursive && not (noccur_between n ntypes b) then
-	        raise (InductiveError BadEntry);
+                raise (InductiveError Type_errors.BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
                 check_constr_rec ienv' nmr' (recarg::lrec) d
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7810c1723e..1b8e4208ff 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,28 +9,9 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Declarations
 open Environ
 open Entries
 
 (** Check an inductive. *)
 val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** Deprecated *)
-type inductive_error =
-  | NonPos of env * constr * constr
-  | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * Id.t * constr * constr * int * int
-  | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of Id.t
-  | SameNamesConstructors of Id.t
-  | SameNamesOverlap of Id.t list
-  | NotAnArity of env * constr
-  | BadEntry
-  | LargeNonPropInductiveNotInType
-  | BadUnivs
-[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
-
-exception InductiveError of Type_errors.inductive_error
-[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
diff --git a/kernel/names.ml b/kernel/names.ml
index 9f27212967..047a1d6525 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -376,9 +376,6 @@ module KerName = struct
     { modpath; knlabel; refhash = -1; }
   let repr kn = (kn.modpath, kn.knlabel)
 
-  let make2 = make
-  [@@ocaml.deprecated "Please use [KerName.make]"]
-
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 61df3bad0e..2238e932b0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -278,9 +278,6 @@ sig
   val make : ModPath.t -> Label.t -> t
   val repr : t -> ModPath.t * Label.t
 
-  val make2 : ModPath.t -> Label.t -> t
-  [@@ocaml.deprecated "Please use [KerName.make]"]
-
   (** Projections *)
   val modpath : t -> ModPath.t
   val label : t -> Label.t
-- 
cgit v1.2.3


From 3c6ed7485293c7eb80f9c4d415af0ee0b977f157 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 3 May 2019 00:41:55 +0200
Subject: Generalize map_named_val to handle whole declarations.

---
 kernel/environ.ml  | 2 +-
 kernel/environ.mli | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 97c9f8654a..617519a038 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with
 let map_named_val f ctxt =
   let open Context.Named.Declaration in
   let fold accu d =
-    let d' = map_constr f d in
+    let d' = f d in
     let accu =
       if d == d' then accu
       else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8c6bc105c7..4e6dbbe206 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -134,9 +134,9 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t
 
 (** [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
-   *** /!\ ***   [f t] should be convertible with t *)
+   *** /!\ ***   [f t] should be convertible with t, and preserve the name *)
 val map_named_val :
-   (constr -> constr) -> named_context_val -> named_context_val
+   (named_declaration -> named_declaration) -> named_context_val -> named_context_val
 
 val push_named : Constr.named_declaration -> env -> env
 val push_named_context : Constr.named_context -> env -> env
-- 
cgit v1.2.3


From 106a7c4a86e4c164a73cbc5a4c14f3c4ff527f30 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 12 May 2019 23:43:01 +0200
Subject: Reduce the attack surface of Opaqueproof.

---
 kernel/modops.ml       |  6 +-----
 kernel/opaqueproof.ml  | 29 +++++++++--------------------
 kernel/opaqueproof.mli |  4 +---
 3 files changed, 11 insertions(+), 28 deletions(-)

(limited to 'kernel')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4f992d3972..4fdd7ab334 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign =
 (** {6 Stm machinery } *)
 let join_constant_body except otab cb =
   match cb.const_body with
-  | OpaqueDef o ->
-      (match Opaqueproof.uuid_opaque otab o with
-      | Some uuid when not(Future.UUIDSet.mem uuid except) ->
-          Opaqueproof.join_opaque otab o
-      | _ -> ())
+  | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o
   | _ -> ()
 
 let join_structure except otab s =
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 303cb06c55..57059300b8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -87,19 +87,18 @@ let discharge_direct_opaque ~cook_constr ci = function
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> ignore(Future.join cu)
+let join except cu = match except with
+| None -> ignore (Future.join cu)
+| Some except ->
+  if Future.UUIDSet.mem (Future.uuid cu) except then ()
+  else ignore (Future.join cu)
+
+let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
+  | Direct (_,cu) -> join except cu
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
         let fp = snd (Int.Map.find i prfs) in
-        ignore(Future.join fp)
-
-let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some (Future.uuid cu)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some (Future.uuid (snd (Int.Map.find i prfs)))
-      else None
+        join except fp
 
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
@@ -128,16 +127,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
       then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
-let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Future.chain cu fst
-  | Indirect (l,dp,i) ->
-      let pt =
-        if DirPath.equal dp odp
-        then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
-      Future.chain pt (fun c ->
-        force_constr (List.fold_right subst_substituted l (from_val c)))
- 
 module FMap = Future.UUIDMap
 
 let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5ea6da649b..d47c0bbb3c 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,7 +39,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_proof : opaquetab -> opaque -> constr Future.computation
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
@@ -60,8 +59,7 @@ type cooking_info = {
 val discharge_direct_opaque :
   cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
 
-val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
-val join_opaque : opaquetab -> opaque -> unit
+val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : opaquetab ->
   Constr.t Future.computation array *
-- 
cgit v1.2.3


From e74fce3090323b4d3734f84ee8cf6dc1f5e85953 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 May 2019 00:03:36 +0200
Subject: Abstract away the implementation of side-effects in Safe_typing.

---
 kernel/entries.ml      | 14 --------------
 kernel/safe_typing.ml  | 29 ++++++++++++++++++++++-------
 kernel/safe_typing.mli |  8 +++-----
 3 files changed, 25 insertions(+), 26 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index a3d32267a7..adb3f6bd29 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -108,21 +108,7 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-
-type seff_env =
-  [ `Nothing
-  (* The proof term and its universes.
-     Same as the constant_body's but not in an ephemeron *)
-  | `Opaque of Constr.t * Univ.ContextSet.t ]
-
 (** Not used by the kernel. *)
 type side_effect_role =
   | Subproof
   | Schema of inductive * string
-
-type side_eff = {
-  seff_constant : Constant.t;
-  seff_body : Declarations.constant_body;
-  seff_env : seff_env;
-  seff_role : side_effect_role;
-}
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 673f025c75..7b573e3146 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,6 +228,12 @@ let check_engagement env expected_impredicative_set =
 
 (** {6 Stm machinery } *)
 
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.ContextSet.t ]
+
 let get_opaque_body env cbo =
   match cbo.const_body with
   | Undef _ -> assert false
@@ -238,9 +244,16 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
+type side_eff = {
+  seff_constant : Constant.t;
+  seff_body : Declarations.constant_body;
+  seff_env : seff_env;
+  seff_role : Entries.side_effect_role;
+}
+
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
-  eff      : Entries.side_eff list;
+  eff      : side_eff list;
 }
 
 module SideEffects :
@@ -254,7 +267,6 @@ end =
 struct
 
 module SeffOrd = struct
-open Entries
 type t = side_effect
 let compare e1 e2 =
   let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
@@ -282,6 +294,14 @@ let side_effects_of_private_constants l =
   let ans = List.rev (SideEffects.repr l) in
   List.map_append (fun { eff; _ } -> eff) ans
 
+let push_private_constants env eff =
+  let eff = side_effects_of_private_constants eff in
+  let add_if_undefined env eff =
+    try ignore(Environ.lookup_constant eff.seff_constant env); env
+    with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+  in
+  List.fold_left add_if_undefined env eff
+
 let empty_private_constants = SideEffects.empty
 let add_private mb eff effs =
   let from_env = CEphemeron.create mb in
@@ -289,7 +309,6 @@ let add_private mb eff effs =
 let concat_private = SideEffects.concat
 
 let make_eff env cst r =
-  let open Entries in
   let cbo = Environ.lookup_constant cst env.env in
   {
     seff_constant = cst;
@@ -309,7 +328,6 @@ let private_con_of_scheme ~kind env cl =
   add_private env.revstruct eff empty_private_constants
 
 let universes_of_private eff =
-  let open Entries in
   let fold acc eff =
     let acc = match eff.seff_env with
     | `Nothing -> acc
@@ -588,7 +606,6 @@ let add_constant_aux ~in_section senv (kn, cb) =
 let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
 
 let inline_side_effects env body side_eff =
-  let open Entries in
   let open Constr in
   (** First step: remove the constants that are still in the environment *)
   let filter { eff = se; from_env = mb } =
@@ -725,7 +742,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_inline_code = cb.const_inline_code }
 
 let turn_direct orig =
-  let open Entries in
   let cb = orig.seff_body in
   if Declareops.is_opaque cb then
     let p = match orig.seff_env with
@@ -738,7 +754,6 @@ let turn_direct orig =
   else orig
 
 let export_eff eff =
-  let open Entries in
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
 let export_side_effects mb env c =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46c97c1fb8..6fcdef9a10 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,11 +43,6 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 type private_constants
 
-val side_effects_of_private_constants :
-  private_constants -> Entries.side_eff list
-(** Return the list of individual side-effects in the order of their
-    creation. *)
-
 val empty_private_constants : private_constants
 val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
@@ -62,6 +57,9 @@ val inline_private_constants_in_constr :
 val inline_private_constants_in_definition_entry :
   Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
 
+val push_private_constants : Environ.env -> private_constants -> Environ.env
+(** Push the constants in the environment if not already there. *)
+
 val universes_of_private : private_constants -> Univ.ContextSet.t list
 
 val is_curmod_library : safe_environment -> bool
-- 
cgit v1.2.3


From 3cdaffab75414f3f59386a4b76c6b00c94bc8b0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 May 2019 00:26:56 +0200
Subject: Simplify the private constant API.

We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
---
 kernel/safe_typing.ml  | 102 ++++++++++++++++++++-----------------------------
 kernel/safe_typing.mli |   4 +-
 2 files changed, 43 insertions(+), 63 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7b573e3146..75375812c0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -244,18 +244,14 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
-type side_eff = {
+type side_effect = {
+  from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
   seff_body : Declarations.constant_body;
   seff_env : seff_env;
   seff_role : Entries.side_effect_role;
 }
 
-type side_effect = {
-  from_env : Declarations.structure_body CEphemeron.key;
-  eff      : side_eff list;
-}
-
 module SideEffects :
 sig
   type t
@@ -269,8 +265,7 @@ struct
 module SeffOrd = struct
 type t = side_effect
 let compare e1 e2 =
-  let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
-  List.compare cmp e1.eff e2.eff
+  Constant.CanOrd.compare e1.seff_constant e2.seff_constant
 end
 
 module SeffSet = Set.Make(SeffOrd)
@@ -291,8 +286,7 @@ end
 type private_constants = SideEffects.t
 
 let side_effects_of_private_constants l =
-  let ans = List.rev (SideEffects.repr l) in
-  List.map_append (fun { eff; _ } -> eff) ans
+  List.rev (SideEffects.repr l)
 
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
@@ -303,29 +297,24 @@ let push_private_constants env eff =
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
-let add_private mb eff effs =
-  let from_env = CEphemeron.create mb in
-  SideEffects.add { eff; from_env } effs
 let concat_private = SideEffects.concat
 
-let make_eff env cst r =
+let private_constant env role cst =
+  (** The constant must be the last entry of the safe environment *)
+  let () = match env.revstruct with
+  | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
+  | _ -> assert false
+  in
+  let from_env = CEphemeron.create env.revstruct in
   let cbo = Environ.lookup_constant cst env.env in
-  {
+  let eff = {
+    from_env = from_env;
     seff_constant = cst;
     seff_body = cbo;
     seff_env = get_opaque_body env.env cbo;
-    seff_role = r;
-  }
-
-let private_con_of_con env c =
-  let open Entries in
-  let eff = [make_eff env c Subproof] in
-  add_private env.revstruct eff empty_private_constants
-
-let private_con_of_scheme ~kind env cl =
-  let open Entries in
-  let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
-  add_private env.revstruct eff empty_private_constants
+    seff_role = role;
+  } in
+  SideEffects.add eff empty_private_constants
 
 let universes_of_private eff =
   let fold acc eff =
@@ -608,19 +597,15 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
 let inline_side_effects env body side_eff =
   let open Constr in
   (** First step: remove the constants that are still in the environment *)
-  let filter { eff = se; from_env = mb } =
-    let map e = (e.seff_constant, e.seff_body, e.seff_env) in
-    let cbl = List.map map se in
-    let not_exists (c,_,_) =
-      try ignore(Environ.lookup_constant c env); false
-      with Not_found -> true in
-    let cbl = List.filter not_exists cbl in
-    (cbl, mb)
+  let filter e =
+    let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+    try ignore (Environ.lookup_constant e.seff_constant env); None
+    with Not_found -> Some (cb, e.from_env)
   in
   (* CAVEAT: we assure that most recent effects come first *)
-  let side_eff = List.map filter (SideEffects.repr side_eff) in
-  let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
-  let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
+  let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
+  let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in
+  let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in
   let side_eff = List.rev side_eff in
   (** Most recent side-effects first in side_eff *)
   if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
@@ -692,24 +677,22 @@ let inline_private_constants_in_definition_entry env ce =
 let inline_private_constants_in_constr env body side_eff =
   pi1 (inline_side_effects env body side_eff)
 
-let rec is_nth_suffix n l suf =
-  if Int.equal n 0 then l == suf
-  else match l with
-  | [] -> false
-  | _ :: l -> is_nth_suffix (pred n) l suf
+let is_suffix l suf = match l with
+| [] -> false
+| _ :: l -> l == suf
 
 (* Given the list of signatures of side effects, checks if they match.
  * I.e. if they are ordered descendants of the current revstruct.
    Returns the number of effects that can be trusted. *)
 let check_signatures curmb sl =
-  let is_direct_ancestor accu (mb, how_many) =
+  let is_direct_ancestor accu mb =
     match accu with
     | None -> None
     | Some (n, curmb) ->
         try
           let mb = CEphemeron.get mb in
-          if is_nth_suffix how_many mb curmb
-          then Some (n + how_many, mb)
+          if is_suffix mb curmb
+          then Some (n + 1, mb)
           else None
         with CEphemeron.InvalidKey -> None in
   let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
@@ -766,10 +749,9 @@ let export_side_effects mb env c =
       let not_exists e =
         try ignore(Environ.lookup_constant e.seff_constant env); false
         with Not_found -> true in
-      let aux (acc,sl) { eff = se; from_env = mb } =
-        let cbl = List.filter not_exists se in
-        if List.is_empty cbl then acc, sl
-        else cbl :: acc, (mb,List.length cbl) :: sl in
+      let aux (acc,sl) e =
+        if not (not_exists e) then acc, sl
+        else e :: acc, e.from_env :: sl in
       let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
       let trusted = check_signatures mb signatures in
       let push_seff env eff =
@@ -787,10 +769,9 @@ let export_side_effects mb env c =
       let rec translate_seff sl seff acc env =
         match seff with
         | [] -> List.rev acc, ce
-        | cbs :: rest ->
+        | eff :: rest ->
           if Int.equal sl 0 then
-           let env, cbs =
-             List.fold_left (fun (env,cbs) eff ->
+           let env, cb =
               let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
                let ce = constant_entry_of_side_effect ocb u in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
@@ -798,15 +779,14 @@ let export_side_effects mb env c =
                 seff_body = cb;
                 seff_env = `Nothing;
                } in
-               (push_seff env eff, export_eff eff :: cbs))
-             (env,[]) cbs in
-           translate_seff 0 rest (cbs @ acc) env
+               (push_seff env eff, export_eff eff)
+            in
+            translate_seff 0 rest (cb :: acc) env
           else
-           let cbs_len = List.length cbs in
-           let cbs = List.map turn_direct cbs in
-           let env = List.fold_left push_seff env cbs in
-           let ecbs = List.map export_eff cbs in
-           translate_seff (sl - cbs_len) rest (ecbs @ acc) env
+           let cb = turn_direct eff in
+           let env = push_seff env cb in
+           let ecb = export_eff cb in
+           translate_seff (sl - 1) rest (ecb :: acc) env
      in
        translate_seff trusted seff [] env
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6fcdef9a10..d6c7022cf5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,8 +48,8 @@ val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
 
-val private_con_of_con : safe_environment -> Constant.t -> private_constants
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants
+val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
+(** Constant must be the last definition of the safe_environment. *)
 
 val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
-- 
cgit v1.2.3


From 93aa8aad110a2839d16dce53af12f0728b59ed2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 14 May 2019 20:27:24 +0200
Subject: Merge the definition of constants and private constants in the API.

---
 kernel/safe_typing.ml  | 8 ++++++--
 kernel/safe_typing.mli | 7 ++-----
 2 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 75375812c0..f2e7cff8ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -797,7 +797,7 @@ let export_private_constants ~in_section ce senv =
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_constant ~in_section l decl senv =
+let add_constant ?role ~in_section l decl senv =
   let kn = Constant.make2 senv.modpath l in
   let senv =
     let cb = 
@@ -822,7 +822,11 @@ let add_constant ~in_section l decl senv =
       add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
     | _ -> senv
   in
-  kn, senv
+  let eff = match role with
+  | None -> empty_private_constants
+  | Some role -> private_constant senv role kn
+  in
+  (kn, eff), senv
 
 (** Insertion of inductive types *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index d6c7022cf5..b9a68663d3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -48,9 +48,6 @@ val concat_private : private_constants -> private_constants -> private_constants
 (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
     [e1] must be more recent than those of [e2]. *)
 
-val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
-(** Constant must be the last definition of the safe_environment. *)
-
 val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
 val inline_private_constants_in_constr :
   Environ.env -> Constr.constr -> private_constants -> Constr.constr
@@ -103,8 +100,8 @@ val export_private_constants : in_section:bool ->
 (** returns the main constant plus a list of auxiliary constants (empty
     unless one requires the side effects to be exported) *)
 val add_constant :
-  in_section:bool -> Label.t -> global_declaration ->
-    Constant.t safe_transformer
+  ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
+    (Constant.t * private_constants) safe_transformer
 
 (** Adding an inductive type *)
 
-- 
cgit v1.2.3


From 925778ff0128dfbfe00aafa8a4aa9f3a2eb2301d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 17:00:57 +0200
Subject: Make the type of constant bodies parametric on opaque proofs.

---
 kernel/cClosure.ml     | 2 +-
 kernel/cClosure.mli    | 2 +-
 kernel/cbytegen.mli    | 2 +-
 kernel/cooking.ml      | 2 +-
 kernel/cooking.mli     | 2 +-
 kernel/declarations.ml | 6 +++---
 6 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 412637c4b6..95f88c0306 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -389,7 +389,7 @@ type clos_infos = {
   i_flags : reds;
   i_cache : infos_cache }
 
-type clos_tab = fconstr constant_def KeyTable.t
+type clos_tab = (fconstr, Empty.t) constant_def KeyTable.t
 
 let info_flags info = info.i_flags
 let info_env info = info.i_cache.i_env
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b1b69dded8..1a790eaed6 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -215,7 +215,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** Conversion auxiliary functions to do step by step normalisation *)
 
 (** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def
+val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def
 
 (***********************************************************************
   i This is for lazy debug *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 6a9550342c..bdaf5fe422 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
-  env -> universes -> Constr.t Mod_subst.substituted constant_def ->
+  env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def ->
   body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9b974c4ecc..19da63b4d4 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -156,7 +156,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
 type result = {
-  cook_body : constr Mod_subst.substituted constant_def;
+  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index b0f143c47d..d218dd36da 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,7 +18,7 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
 type result = {
-  cook_body : constr Mod_subst.substituted constant_def;
+  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5551742c02..649bb8725d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,10 +47,10 @@ type inline = int option
     transparent body, or an opaque one *)
 
 (* Global declarations (i.e. constants) can be either: *)
-type 'a constant_def =
+type ('a, 'opaque) constant_def =
   | Undef of inline                       (** a global assumption *)
   | Def of 'a                             (** or a transparent global definition *)
-  | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
+  | OpaqueDef of 'opaque                  (** or an opaque global definition *)
   | Primitive of CPrimitives.t            (** or a primitive operation *)
 
 type universes =
@@ -89,7 +89,7 @@ type typing_flags = {
  * the OpaqueDef *)
 type constant_body = {
     const_hyps : Constr.named_context; (** New: younger hyp at top *)
-    const_body : Constr.t Mod_subst.substituted constant_def;
+    const_body : (Constr.t Mod_subst.substituted, Opaqueproof.opaque) constant_def;
     const_type : types;
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
-- 
cgit v1.2.3


From 801aed67a90ec49c15a4469e1905aa2835fabe19 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 May 2019 23:50:42 +0200
Subject: Parameterize the constant_body type by opaque subproofs.

---
 kernel/cooking.ml      |  2 +-
 kernel/cooking.mli     |  2 +-
 kernel/declarations.ml |  6 +++---
 kernel/declareops.mli  | 12 ++++++------
 kernel/environ.ml      |  2 +-
 kernel/environ.mli     | 12 ++++++------
 kernel/nativecode.mli  |  2 +-
 kernel/safe_typing.ml  |  2 +-
 kernel/subtyping.ml    |  2 +-
 kernel/term_typing.mli |  6 +++---
 10 files changed, 24 insertions(+), 24 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 19da63b4d4..d879f4ee95 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -152,7 +152,7 @@ let abstract_constant_body c (hyps, subst) =
   let c = Vars.subst_vars subst c in
   it_mkLambda_or_LetIn c hyps
 
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
 type result = {
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index d218dd36da..ffd4e51ffc 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -13,7 +13,7 @@ open Declarations
 
 (** {6 Cooking the constants. } *)
 
-type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
+type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 
 type inline = bool
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 649bb8725d..36ee952099 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -87,9 +87,9 @@ type typing_flags = {
 
 (* some contraints are in constant_constraints, some other may be in
  * the OpaqueDef *)
-type constant_body = {
+type 'opaque constant_body = {
     const_hyps : Constr.named_context; (** New: younger hyp at top *)
-    const_body : (Constr.t Mod_subst.substituted, Opaqueproof.opaque) constant_def;
+    const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
     const_type : types;
     const_relevance : Sorts.relevance;
     const_body_code : Cemitcodes.to_patch_substituted option;
@@ -246,7 +246,7 @@ type module_alg_expr =
 (** A component of a module structure *)
 
 type structure_field_body =
-  | SFBconst of constant_body
+  | SFBconst of Opaqueproof.opaque constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 54a853fc81..fb02c6a029 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -26,21 +26,21 @@ val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
 
 (** {6 Constants} *)
 
-val subst_const_body : substitution -> constant_body -> constant_body
+val subst_const_body : substitution -> Opaqueproof.opaque constant_body -> Opaqueproof.opaque constant_body
 
 (** Is there a actual body in const_body ? *)
 
-val constant_has_body : constant_body -> bool
+val constant_has_body : 'a constant_body -> bool
 
-val constant_polymorphic_context : constant_body -> AUContext.t
+val constant_polymorphic_context : 'a constant_body -> AUContext.t
 
 (** Is the constant polymorphic? *)
-val constant_is_polymorphic : constant_body -> bool
+val constant_is_polymorphic : 'a constant_body -> bool
 
 (** Return the universe context, in case the definition is polymorphic, otherwise
     the context is empty. *)
 
-val is_opaque : constant_body -> bool
+val is_opaque : 'a constant_body -> bool
 
 (** {6 Inductive types} *)
 
@@ -83,7 +83,7 @@ val safe_flags : Conv_oracle.oracle -> typing_flags
     of the structure, but simply hash-cons all inner constr
     and other known elements *)
 
-val hcons_const_body : constant_body -> constant_body
+val hcons_const_body : 'a constant_body -> 'a constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
 val hcons_module_body : module_body -> module_body
 val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 97c9f8654a..67125e9ad1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,7 +46,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8c6bc105c7..6d3756e891 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -42,7 +42,7 @@ type link_info =
 
 type key = int CEphemeron.key option ref
 
-type constant_key = constant_body * (link_info ref * key)
+type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
 
 type mind_key = mutual_inductive_body * link_info ref
 
@@ -174,19 +174,19 @@ val reset_with_named_context : named_context_val -> env -> env
 val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
-val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
-val add_constant : Constant.t -> constant_body -> env -> env
-val add_constant_key : Constant.t -> constant_body -> link_info ->
+val add_constant : Constant.t -> Opaqueproof.opaque constant_body -> env -> env
+val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_info ->
   env -> env
 val lookup_constant_key :  Constant.t -> env -> constant_key
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
-val lookup_constant    : Constant.t -> env -> constant_body
+val lookup_constant    : Constant.t -> env -> Opaqueproof.opaque constant_body
 val evaluable_constant : Constant.t -> env -> bool
 
 (** New-style polymorphism *)
@@ -219,7 +219,7 @@ val constant_context : env -> Constant.t -> Univ.AUContext.t
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
-val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 96efa7faa5..b5c03b6ca3 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val empty_updates : code_location_updates
 val register_native_file : string -> unit
 
 val compile_constant_field : env -> string -> Constant.t ->
-  global list -> constant_body -> global list
+  global list -> 'a constant_body -> global list
 
 val compile_mind_field : ModPath.t -> Label.t ->
   global list -> mutual_inductive_body -> global list
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f2e7cff8ec..36f1515a8c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -247,7 +247,7 @@ let get_opaque_body env cbo =
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
-  seff_body : Declarations.constant_body;
+  seff_body : Opaqueproof.opaque Declarations.constant_body;
   seff_env : seff_env;
   seff_role : Entries.side_effect_role;
 }
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1857ea3329..24845ce459 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -31,7 +31,7 @@ open Mod_subst
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
 type namedobject =
-  | Constant of constant_body
+  | Constant of Opaqueproof.opaque constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1fa5eca2e3..01b69b2b66 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -33,9 +33,9 @@ val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
-    constant_body
+    Opaqueproof.opaque constant_body
 
-val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
+val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
@@ -43,4 +43,4 @@ val infer_declaration : trust:'a trust -> env ->
   'a constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  Constant.t -> env -> Cooking.result -> constant_body
+  Constant.t -> env -> Cooking.result -> Opaqueproof.opaque constant_body
-- 
cgit v1.2.3


From 27468ae02bbbf018743d53a9db49efa34b6d6a3e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 00:02:54 +0200
Subject: Ensure statically that declarations built by Term_typing are direct.

This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
---
 kernel/cooking.ml      |   4 +-
 kernel/cooking.mli     |   6 +-
 kernel/opaqueproof.ml  |   4 ++
 kernel/opaqueproof.mli |   1 +
 kernel/safe_typing.ml  | 146 ++++++++++++++++++++++---------------------------
 kernel/safe_typing.mli |   4 +-
 kernel/term_typing.ml  |  44 ++++++++-------
 kernel/term_typing.mli |   8 ++-
 8 files changed, 106 insertions(+), 111 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index d879f4ee95..9b6e37251f 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -155,8 +155,8 @@ let abstract_constant_body c (hyps, subst) =
 type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cooking_info }
 type inline = bool
 
-type result = {
-  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
+type 'opaque result = {
+  cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index ffd4e51ffc..b022e2ac09 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -17,8 +17,8 @@ type recipe = { from : Opaqueproof.opaque constant_body; info : Opaqueproof.cook
 
 type inline = bool
 
-type result = {
-  cook_body : (constr Mod_subst.substituted, Opaqueproof.opaque) constant_def;
+type 'opaque result = {
+  cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
   cook_type : types;
   cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
@@ -27,7 +27,7 @@ type result = {
   cook_context : Constr.named_context option;
 }
 
-val cook_constant : hcons:bool -> recipe -> result
+val cook_constant : hcons:bool -> recipe -> Opaqueproof.opaque result
 val cook_constr : Opaqueproof.cooking_info -> constr -> constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 57059300b8..423a416ca4 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -100,6 +100,10 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
+let force_direct = function
+| Direct (_, cu) -> Future.force cu
+| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
+
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index d47c0bbb3c..8b6e8a1c8f 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,6 +39,7 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
+val force_direct : opaque -> (constr * Univ.ContextSet.t)
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 36f1515a8c..a5d8a480ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,27 +228,10 @@ let check_engagement env expected_impredicative_set =
 
 (** {6 Stm machinery } *)
 
-type seff_env =
-  [ `Nothing
-  (* The proof term and its universes.
-     Same as the constant_body's but not in an ephemeron *)
-  | `Opaque of Constr.t * Univ.ContextSet.t ]
-
-let get_opaque_body env cbo =
-  match cbo.const_body with
-  | Undef _ -> assert false
-  | Primitive _ -> assert false
-  | Def _ -> `Nothing
-  | OpaqueDef opaque ->
-      `Opaque
-        (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
-         Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-
 type side_effect = {
   from_env : Declarations.structure_body CEphemeron.key;
   seff_constant : Constant.t;
-  seff_body : Opaqueproof.opaque Declarations.constant_body;
-  seff_env : seff_env;
+  seff_body : (Constr.t * Univ.ContextSet.t) Declarations.constant_body;
   seff_role : Entries.side_effect_role;
 }
 
@@ -288,39 +271,38 @@ type private_constants = SideEffects.t
 let side_effects_of_private_constants l =
   List.rev (SideEffects.repr l)
 
+(* Only used to push in an Environ.env. *)
+let lift_constant c =
+  let body = match c.const_body with
+  | OpaqueDef _ -> Undef None
+  | Def _ | Undef _ | Primitive _ as body -> body
+  in
+  { c with const_body = body }
+
+let map_constant f c =
+  let body = match c.const_body with
+  | OpaqueDef o -> OpaqueDef (f o)
+  | Def _ | Undef _ | Primitive _ as body -> body
+  in
+  { c with const_body = body }
+
 let push_private_constants env eff =
   let eff = side_effects_of_private_constants eff in
   let add_if_undefined env eff =
     try ignore(Environ.lookup_constant eff.seff_constant env); env
-    with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+    with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env
   in
   List.fold_left add_if_undefined env eff
 
 let empty_private_constants = SideEffects.empty
 let concat_private = SideEffects.concat
 
-let private_constant env role cst =
-  (** The constant must be the last entry of the safe environment *)
-  let () = match env.revstruct with
-  | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
-  | _ -> assert false
-  in
-  let from_env = CEphemeron.create env.revstruct in
-  let cbo = Environ.lookup_constant cst env.env in
-  let eff = {
-    from_env = from_env;
-    seff_constant = cst;
-    seff_body = cbo;
-    seff_env = get_opaque_body env.env cbo;
-    seff_role = role;
-  } in
-  SideEffects.add eff empty_private_constants
-
 let universes_of_private eff =
   let fold acc eff =
-    let acc = match eff.seff_env with
-    | `Nothing -> acc
-    | `Opaque (_, ctx) -> ctx :: acc
+    let acc = match eff.seff_body.const_body with
+    | Def _ -> acc
+    | OpaqueDef (_, ctx) -> ctx :: acc
+    | Primitive _ | Undef _ -> assert false
     in
     match eff.seff_body.const_universes with
     | Monomorphic ctx -> ctx :: acc
@@ -565,7 +547,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -598,7 +579,7 @@ let inline_side_effects env body side_eff =
   let open Constr in
   (** First step: remove the constants that are still in the environment *)
   let filter e =
-    let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+    let cb = (e.seff_constant, e.seff_body) in
     try ignore (Environ.lookup_constant e.seff_constant env); None
     with Not_found -> Some (cb, e.from_env)
   in
@@ -612,10 +593,10 @@ let inline_side_effects env body side_eff =
   else
     (** Second step: compute the lifts and substitutions to apply *)
     let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in
-    let fold (subst, var, ctx, args) (c, cb, b) =
-      let (b, opaque) = match cb.const_body, b with
-      | Def b, _ -> (Mod_subst.force_constr b, false)
-      | OpaqueDef _, `Opaque (b,_) -> (b, true)
+    let fold (subst, var, ctx, args) (c, cb) =
+      let (b, opaque) = match cb.const_body with
+      | Def b -> (Mod_subst.force_constr b, false)
+      | OpaqueDef (b, _) -> (b, true)
       | _ -> assert false
       in
       match cb.const_universes with
@@ -701,7 +682,8 @@ let check_signatures curmb sl =
   | Some (n, _) -> n
 
 
-let constant_entry_of_side_effect cb u =
+let constant_entry_of_side_effect eff =
+  let cb = eff.seff_body in
   let open Entries in
   let univs =
     match cb.const_universes with
@@ -711,9 +693,9 @@ let constant_entry_of_side_effect cb u =
       Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
   in
   let pt =
-    match cb.const_body, u with
-    | OpaqueDef _, `Opaque (b, c) -> b, c
-    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    match cb.const_body with
+    | OpaqueDef (b, c) -> b, c
+    | Def b -> Mod_subst.force_constr b, Univ.ContextSet.empty
     | _ -> assert false in
   DefinitionEntry {
     const_entry_body = Future.from_val (pt, ());
@@ -724,18 +706,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
 
-let turn_direct orig =
-  let cb = orig.seff_body in
-  if Declareops.is_opaque cb then
-    let p = match orig.seff_env with
-    | `Opaque (b, c) -> (b, c)
-    | _ -> assert false
-    in
-    let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in
-    let cb = { cb with const_body } in
-    { orig with seff_body = cb }
-  else orig
-
 let export_eff eff =
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
@@ -756,13 +726,14 @@ let export_side_effects mb env c =
       let trusted = check_signatures mb signatures in
       let push_seff env eff =
         let { seff_constant = kn; seff_body = cb ; _ } = eff in
-        let env = Environ.add_constant kn cb env in
+        let env = Environ.add_constant kn (lift_constant cb) env in
         match cb.const_universes with
         | Polymorphic _ -> env
         | Monomorphic ctx ->
-          let ctx = match eff.seff_env with
-          | `Nothing -> ctx
-          | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
+          let ctx = match eff.seff_body.const_body with
+          | Def _ -> ctx
+          | OpaqueDef (_, ctx') -> Univ.ContextSet.union ctx' ctx
+          | Undef _ | Primitive _ -> assert false
           in
           Environ.push_context_set ~strict:true ctx env
       in
@@ -771,35 +742,39 @@ let export_side_effects mb env c =
         | [] -> List.rev acc, ce
         | eff :: rest ->
           if Int.equal sl 0 then
-           let env, cb =
-              let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
-               let ce = constant_entry_of_side_effect ocb u in
+            let env, cb =
+              let kn = eff.seff_constant in
+               let ce = constant_entry_of_side_effect eff in
                let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
-               let eff = { eff with
-                seff_body = cb;
-                seff_env = `Nothing;
-               } in
+               let cb = map_constant Future.force cb in
+               let eff = { eff with seff_body = cb } in
                (push_seff env eff, export_eff eff)
             in
             translate_seff 0 rest (cb :: acc) env
           else
-           let cb = turn_direct eff in
-           let env = push_seff env cb in
-           let ecb = export_eff cb in
+           let env = push_seff env eff in
+           let ecb = export_eff eff in
            translate_seff (sl - 1) rest (ecb :: acc) env
      in
        translate_seff trusted seff [] env
 
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in
+  let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in
+  let bodies = List.map map exported in
   let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
+let add_recipe ~in_section l r senv =
+  let kn = Constant.make2 senv.modpath l in
+  let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
+  let cb = if in_section then cb else Declareops.hcons_const_body cb in
+  let senv = add_constant_aux ~in_section senv (kn, cb) in
+  kn, senv
+
 let add_constant ?role ~in_section l decl senv =
   let kn = Constant.make2 senv.modpath l in
-  let senv =
     let cb = 
       match decl with
       | ConstantEntry (EffectEntry, ce) ->
@@ -811,9 +786,9 @@ let add_constant ?role ~in_section l decl senv =
         Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce
       | ConstantEntry (PureEntry, ce) ->
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
-      | GlobalRecipe r ->
-        let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in
-        if in_section then cb else Declareops.hcons_const_body cb in
+    in
+  let senv =
+    let cb = map_constant Opaqueproof.create cb in
     add_constant_aux ~in_section senv (kn, cb) in
   let senv =
     match decl with
@@ -824,7 +799,16 @@ let add_constant ?role ~in_section l decl senv =
   in
   let eff = match role with
   | None -> empty_private_constants
-  | Some role -> private_constant senv role kn
+  | Some role ->
+    let cb = map_constant Future.force cb in
+    let from_env = CEphemeron.create senv.revstruct in
+    let eff = {
+      from_env = from_env;
+      seff_constant = kn;
+      seff_body = cb;
+      seff_role = role;
+    } in
+    SideEffects.add eff empty_private_constants
   in
   (kn, eff), senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b9a68663d3..36ca3d8c47 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -88,7 +88,6 @@ type 'a effect_entry =
 
 type global_declaration =
   | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
-  | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
   Constant.t * Entries.side_effect_role
@@ -103,6 +102,9 @@ val add_constant :
   ?role:Entries.side_effect_role -> in_section:bool -> Label.t -> global_declaration ->
     (Constant.t * private_constants) safe_transformer
 
+val add_recipe :
+  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
+
 (** Adding an inductive type *)
 
 val add_mind :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index faa4411e92..9e33b431fc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -154,7 +154,7 @@ the polymorphic case
           let c = Constr.hcons j.uj_val in
           feedback_completion_typecheck feedback_id;
           c, uctx) in
-      let def = OpaqueDef (Opaqueproof.create proofterm) in
+      let def = OpaqueDef proofterm in
       {
         Cooking.cook_body = def;
         cook_type = tyj.utj_val;
@@ -207,7 +207,7 @@ the polymorphic case
       in
       let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
-	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+        if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty))
 	else Def (Mod_subst.from_val def) 
       in
 	feedback_completion_typecheck feedback_id;
@@ -232,7 +232,7 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let build_constant_declaration _kn env result =
+let build_constant_declaration ~force ~iter env result =
   let open Cooking in
   let typ = result.cook_type in
   let check declared inferred =
@@ -271,11 +271,8 @@ let build_constant_declaration _kn env result =
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let vars =
-              global_vars_set env
-                (Opaqueproof.force_proof (opaque_tables env) lc) in
-            (* we force so that cst are added to the env immediately after *)
-            ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
+            let (lc, _) = force lc in
+            let vars = global_vars_set env lc in
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
@@ -296,11 +293,14 @@ let build_constant_declaration _kn env result =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
-            OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set env typ in
-              let ids_def = global_vars_set env c in
-              let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
-              check declared inferred) lc) in
+          let kont c =
+            let ids_typ = global_vars_set env typ in
+            let ids_def = global_vars_set env c in
+            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            check declared inferred
+          in
+          OpaqueDef (iter kont lc)
+  in
   let univs = result.cook_universes in
   let tps = 
     let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
@@ -318,8 +318,10 @@ let build_constant_declaration _kn env result =
 
 (*s Global and local constant declaration. *)
 
-let translate_constant mb env kn ce =
-  build_constant_declaration kn env
+let translate_constant mb env _kn ce =
+  let force cu = Future.force cu in
+  let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
+  build_constant_declaration ~force ~iter env
     (infer_declaration ~trust:mb env ce)
 
 let translate_local_assum env t =
@@ -327,8 +329,10 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     j.uj_val, t
 
-let translate_recipe ~hcons env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
+let translate_recipe ~hcons env _kn r =
+  let force o = Opaqueproof.force_direct o in
+  let iter k o = Opaqueproof.iter_direct_opaque k o in
+  build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r)
 
 let translate_local_def env _id centry =
   let open Cooking in
@@ -351,8 +355,7 @@ let translate_local_def env _id centry =
     | Def _ -> ()
     | OpaqueDef lc ->
        let ids_typ = global_vars_set env typ in
-       let ids_def = global_vars_set env
-         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let ids_def = global_vars_set env (fst (Future.force lc)) in
        record_aux env ids_typ ids_def
   end;
   let () = match decl.cook_universes with
@@ -362,8 +365,7 @@ let translate_local_def env _id centry =
   let c = match decl.cook_body with
   | Def c -> Mod_subst.force_constr c
   | OpaqueDef o ->
-    let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in
-    let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in
+    let (p, cst) = Future.force o in
     (** Let definitions are ensured to have no extra constraints coming from
         the body by virtue of the typing of [Entries.section_def_entry]. *)
     let () = assert (Univ.ContextSet.is_empty cst) in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 01b69b2b66..a046d26ea9 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -33,14 +33,16 @@ val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
-    Opaqueproof.opaque constant_body
+    Opaqueproof.proofterm constant_body
 
 val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
 val infer_declaration : trust:'a trust -> env ->
-  'a constant_entry -> Cooking.result
+  'a constant_entry -> Opaqueproof.proofterm Cooking.result
 
 val build_constant_declaration :
-  Constant.t -> env -> Cooking.result -> Opaqueproof.opaque constant_body
+  force:('a -> constr * 'b) ->
+  iter:((constr -> unit) -> 'a -> 'a) ->
+  env -> 'a Cooking.result -> 'a constant_body
-- 
cgit v1.2.3


From e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 May 2019 14:18:25 +0200
Subject: Do not perform the section variable check on global recipes.

By construction, we know that Cooking is returning the right set of
used variables. This set has been checked already once at the time
when the definition was performed inside the section.
---
 kernel/opaqueproof.ml  |  9 ---------
 kernel/opaqueproof.mli |  2 --
 kernel/term_typing.ml  | 26 ++++++++++++++++++--------
 kernel/term_typing.mli |  4 +---
 4 files changed, 19 insertions(+), 22 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 423a416ca4..18c1bcc0f8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -77,11 +77,6 @@ let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
   | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
 
-let iter_direct_opaque f = function
-  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-  | Direct (d,cu) ->
-      Direct (d,Future.chain cu (fun (c, u) -> f c; c, u))
-
 let discharge_direct_opaque ~cook_constr ci = function
   | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
   | Direct (d,cu) ->
@@ -100,10 +95,6 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
         let fp = snd (Int.Map.find i prfs) in
         join except fp
 
-let force_direct = function
-| Direct (_, cu) -> Future.force cu
-| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 8b6e8a1c8f..4e8956af06 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,12 +39,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val force_direct : opaque -> (constr * Univ.ContextSet.t)
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
-val iter_direct_opaque : (constr -> unit) -> opaque -> opaque
 
 type work_list = (Univ.Instance.t * Id.t array) Cmap.t * 
   (Univ.Instance.t * Id.t array) Mindmap.t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9e33b431fc..74c6189a65 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -232,7 +232,7 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let build_constant_declaration ~force ~iter env result =
+let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
   let check declared inferred =
@@ -271,7 +271,7 @@ let build_constant_declaration ~force ~iter env result =
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
-            let (lc, _) = force lc in
+            let (lc, _) = Future.force lc in
             let vars = global_vars_set env lc in
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
@@ -293,6 +293,7 @@ let build_constant_declaration ~force ~iter env result =
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
+          let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
           let kont c =
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env c in
@@ -319,9 +320,7 @@ let build_constant_declaration ~force ~iter env result =
 (*s Global and local constant declaration. *)
 
 let translate_constant mb env _kn ce =
-  let force cu = Future.force cu in
-  let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in
-  build_constant_declaration ~force ~iter env
+  build_constant_declaration env
     (infer_declaration ~trust:mb env ce)
 
 let translate_local_assum env t =
@@ -330,9 +329,20 @@ let translate_local_assum env t =
     j.uj_val, t
 
 let translate_recipe ~hcons env _kn r =
-  let force o = Opaqueproof.force_direct o in
-  let iter k o = Opaqueproof.iter_direct_opaque k o in
-  build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r)
+  let open Cooking in
+  let result = Cooking.cook_constant ~hcons r in
+  let univs = result.cook_universes in
+  let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
+  let tps = Option.map Cemitcodes.from_val res in
+  { const_hyps = Option.get result.cook_context;
+    const_body = result.cook_body;
+    const_type = result.cook_type;
+    const_body_code = tps;
+    const_universes = univs;
+    const_private_poly_univs = result.cook_private_univs;
+    const_relevance = result.cook_relevance;
+    const_inline_code = result.cook_inline;
+    const_typing_flags = Environ.typing_flags env }
 
 let translate_local_def env _id centry =
   let open Cooking in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index a046d26ea9..592a97e132 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -43,6 +43,4 @@ val infer_declaration : trust:'a trust -> env ->
   'a constant_entry -> Opaqueproof.proofterm Cooking.result
 
 val build_constant_declaration :
-  force:('a -> constr * 'b) ->
-  iter:((constr -> unit) -> 'a -> 'a) ->
-  env -> 'a Cooking.result -> 'a constant_body
+  env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
-- 
cgit v1.2.3