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