From 1f2a3fe97be66fd3201b9c98e5744953d4149b91 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jun 2019 22:04:25 +0200
Subject: Cleaning up the previous code by ensuring statically invariants on
 opaque proofs.

We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
---
 kernel/term_typing.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index f82312245b..c9f6d66e36 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -30,8 +30,12 @@ val translate_local_def : env -> Id.t -> section_def_entry ->
 val translate_local_assum : env -> types -> types * Sorts.relevance
 
 val translate_constant :
-  env -> Constant.t -> 'a constant_entry ->
-    typing_context constant_body
+  env -> Constant.t -> constant_entry ->
+    'a constant_body
+
+val translate_opaque :
+  env -> Constant.t -> 'a opaque_entry ->
+    unit constant_body * typing_context
 
 val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
@@ -40,7 +44,7 @@ val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (C
 (** Internal functions, mentioned here for debug purpose only *)
 
 val infer_declaration : env ->
-  'a constant_entry -> typing_context Cooking.result
+  constant_entry -> typing_context Cooking.result
 
 val build_constant_declaration :
   env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body
-- 
cgit v1.2.3