diff options
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 |