diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index a71587f0f..ba4d96a5f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -41,7 +41,7 @@ val infer_declaration : chkguard:bool -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + chkguard:bool -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit |