diff options
| author | Pierre-Marie Pédrot | 2019-05-17 14:18:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-20 14:11:44 +0200 |
| commit | e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c (patch) | |
| tree | caf9be18ce8da31926142946455fa7982f9d84fd /kernel/term_typing.mli | |
| parent | 27468ae02bbbf018743d53a9db49efa34b6d6a3e (diff) | |
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.
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 4 |
1 files changed, 1 insertions, 3 deletions
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 |