From f22205ee06f9170a74dc8cefba2b42deeaeb246b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 16:04:52 +0200
Subject: Make explicit the delayed computation of opaque bodies in
 Term_typing.

We separate the Term_typing inference API into two functions, one to
typecheck just the immediate part of an entry, and another one to check
after the fact that a delayed term is indeed a correct proof for an opaque
entry.

This commit is mostly moving code around, this should be 1:1 semantically.
---
 kernel/term_typing.mli | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ef01ece185..f82312245b 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,9 +22,7 @@ open Entries
 type 'a effect_handler =
   env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int)
 
-type _ trust =
-| Pure : unit trust
-| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust
+type typing_context
 
 val translate_local_def : env -> Id.t -> section_def_entry ->
   constr * Sorts.relevance * types
@@ -32,15 +30,17 @@ val translate_local_def : env -> Id.t -> section_def_entry ->
 val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
-  'a trust -> env -> Constant.t -> 'a constant_entry ->
-    Opaqueproof.proofterm constant_body
+  env -> Constant.t -> 'a constant_entry ->
+    typing_context constant_body
 
 val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
+val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes)
+
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : trust:'a trust -> env ->
-  'a constant_entry -> Opaqueproof.proofterm Cooking.result
+val infer_declaration : env ->
+  'a constant_entry -> typing_context Cooking.result
 
 val build_constant_declaration :
   env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
-- 
cgit v1.2.3