From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 kernel/term_typing.mli | 41 ++++++++++++++++++++++++++---------------
 1 file changed, 26 insertions(+), 15 deletions(-)

(limited to 'kernel/term_typing.mli')

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
-- 
cgit v1.2.3