diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:09:15 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 15:09:15 +0200 |
| commit | caf8402e4af75d85223e10cba68a6a145e050dab (patch) | |
| tree | e8c3af2139d78b7e0117fd4987b7eb3732381577 /kernel/term_typing.mli | |
| parent | 0b20282c49253aea4429384467b75a5bdb1f8ba4 (diff) | |
Add a field in `constant_body` to track constant whose well-foundedness is assumed.
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 |