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/term_typing.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/term_typing.mli')

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/term_typing.mli | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel/term_typing.mli')

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/term_typing.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/term_typing.mli')

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