diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli new file mode 100644 index 0000000000..1fa5eca2e3 --- /dev/null +++ b/kernel/term_typing.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Constr +open Environ +open Declarations +open Entries + +(** Handlers are used to manage side-effects. The ['a] type stands for the type + of side-effects, and it is parametric because they are only defined later + on. Handlers inline the provided side-effects into the term, and return + the set of additional global constraints that need to be added for the term + to be well typed. *) +type 'a effect_handler = + env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) + +type _ trust = +| Pure : unit trust +| SideEffects : 'a effect_handler -> 'a trust + +val translate_local_def : env -> Id.t -> section_def_entry -> + constr * Sorts.relevance * types + +val translate_local_assum : env -> types -> types * Sorts.relevance + +val translate_constant : + 'a trust -> env -> Constant.t -> 'a constant_entry -> + constant_body + +val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body + +(** Internal functions, mentioned here for debug purpose only *) + +val infer_declaration : trust:'a trust -> env -> + 'a constant_entry -> Cooking.result + +val build_constant_declaration : + Constant.t -> env -> Cooking.result -> constant_body |