diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/term_typing.mli | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 41 |
1 files changed, 26 insertions, 15 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index bcc2ca0d..696fc3d2 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,29 +9,40 @@ open Names open Term open Univ -open Declarations -open Inductive open Environ +open Declarations open Entries -open Typeops -val translate_local_def : env -> constr * types option -> - constr * types * Univ.constraints +val translate_local_def : env -> Id.t -> definition_entry -> + constant_def * types * constant_universes -val translate_local_assum : env -> types -> - types * Univ.constraints +val translate_local_assum : env -> types -> types -val infer_declaration : env -> constant_entry -> - constant_def * constant_type * constraints * Sign.section_context option +val mk_pure_proof : constr -> proof_output -val build_constant_declaration : env -> 'a -> - constant_def * constant_type * constraints * Sign.section_context option -> - constant_body +val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +(** Returns the term where side effects have been turned into let-ins or beta + redexes. *) + +val handle_entry_side_effects : env -> definition_entry -> definition_entry +(** Same as {!handle_side_effects} but applied to entries. Only modifies the + {!Entries.const_entry_body} field. It is meant to get a term out of a not + yet type checked proof. *) val translate_constant : env -> constant -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body -val translate_recipe : - env -> constant -> Cooking.recipe -> constant_body +val translate_recipe : env -> constant -> Cooking.recipe -> constant_body + +(** Internal functions, mentioned here for debug purpose only *) + +val infer_declaration : env -> constant option -> + constant_entry -> Cooking.result + +val build_constant_declaration : + constant -> env -> Cooking.result -> constant_body + +val set_suggest_proof_using : + (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit |