Imported Upstream version 8.5~beta3+dfsg

1 files changed, 32 insertions, 9 deletions

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea..2e6aa161 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,46 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
 val translate_local_assum : env -> types -> types
 
-val mk_pure_proof : constr -> proof_output
+val mk_pure_proof : constr -> side_effects proof_output
 
-val handle_side_effects : env -> constr -> Declareops.side_effects -> constr
+val inline_side_effects : env -> constr -> 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
+val inline_entry_side_effects :
+  env -> side_effects definition_entry -> side_effects definition_entry
+(** Same as {!inline_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 uniq_seff : side_effects -> side_effects
+
+val translate_constant :
+  structure_body -> env -> constant -> side_effects constant_entry ->
+    constant_body
+
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects constant_entry * side_effect_role
+  
+(* Given a constant entry containing side effects it exports them (either
+ * by re-checking them or trusting them).  Returns the constant bodies to
+ * be pushed in the safe_env by safe typing.  The main constant entry
+ * needs to be translated as usual after this step. *)
+val export_side_effects :
+  structure_body -> env -> side_effects constant_entry ->
+    exported_side_effect list * side_effects constant_entry
+
+val constant_entry_of_side_effect :
+  constant_body -> seff_env -> side_effects constant_entry
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,11 +60,11 @@ 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 infer_declaration : trust:structure_body -> env -> constant option -> 
+  side_effects 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
+  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit