diff options
| author | Pierre-Marie Pédrot | 2019-06-28 16:04:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 17:33:25 +0200 |
| commit | f22205ee06f9170a74dc8cefba2b42deeaeb246b (patch) | |
| tree | 8b643e358cdbbc57cfeba13668a21ff3e8e91607 /kernel/term_typing.mli | |
| parent | cc9856e33fa1a15fe699e8d9cd7b76086563683d (diff) | |
Make explicit the delayed computation of opaque bodies in Term_typing.
We separate the Term_typing inference API into two functions, one to
typecheck just the immediate part of an entry, and another one to check
after the fact that a delayed term is indeed a correct proof for an opaque
entry.
This commit is mostly moving code around, this should be 1:1 semantically.
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ef01ece185..f82312245b 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,9 +22,7 @@ open Entries type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust +type typing_context val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types @@ -32,15 +30,17 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - 'a trust -> env -> Constant.t -> 'a constant_entry -> - Opaqueproof.proofterm constant_body + env -> Constant.t -> 'a constant_entry -> + typing_context constant_body val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) + (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Opaqueproof.proofterm Cooking.result +val infer_declaration : env -> + 'a constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |