diff options
| author | Pierre-Marie Pédrot | 2019-06-28 22:04:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 17:38:49 +0200 |
| commit | 1f2a3fe97be66fd3201b9c98e5744953d4149b91 (patch) | |
| tree | 9e1e992d5f2f706505e4184d990f2790e41df6ca /kernel/term_typing.mli | |
| parent | f22205ee06f9170a74dc8cefba2b42deeaeb246b (diff) | |
Cleaning up the previous code by ensuring statically invariants on opaque proofs.
We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index f82312245b..c9f6d66e36 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,8 +30,12 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - env -> Constant.t -> 'a constant_entry -> - typing_context constant_body + env -> Constant.t -> constant_entry -> + 'a constant_body + +val translate_opaque : + env -> Constant.t -> 'a opaque_entry -> + unit constant_body * typing_context val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body @@ -40,7 +44,7 @@ val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (C (** Internal functions, mentioned here for debug purpose only *) val infer_declaration : env -> - 'a constant_entry -> typing_context Cooking.result + constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |