Exporting the function handling side-effects only applied to terms.

kernel/term_typing.ml

@@ -286,7 +286,7 @@ let translate_local_def env id centry =
 
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
-let handle_side_effects env ce = { ce with
+let handle_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       (handle_side_effects env body side_eff, ctx), Declareops.no_seff);

kernel/term_typing.mli

@@ -20,10 +20,14 @@ val translate_local_assum : env -> types -> types
 
 val mk_pure_proof : constr -> proof_output
 
-(* returns the same definition_entry but with side effects turned into
- * let-ins or beta redexes. it is meant to get a term out of a not yet
- * type checked proof *)
-val handle_side_effects : env -> definition_entry -> definition_entry
+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
 

proofs/pfedit.ml

@@ -149,7 +149,7 @@ let build_by_tactic env ctx ?(poly=false) typ tac =
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
-  let ce = Term_typing.handle_side_effects env ce in
+  let ce = Term_typing.handle_entry_side_effects env ce in
   let (cb, ctx), se = Future.force ce.const_entry_body in
   assert(Declareops.side_effects_is_empty se);
   assert(Univ.ContextSet.is_empty ctx);

toplevel/obligations.ml

@@ -780,7 +780,7 @@ let solve_by_tac name evi t poly ctx =
   let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
     id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
   let env = Global.env () in
-  let entry = Term_typing.handle_side_effects env entry in
+  let entry = Term_typing.handle_entry_side_effects env entry in
   let body, eff = Future.force entry.Entries.const_entry_body in
   assert(Declareops.side_effects_is_empty eff);
   assert(Univ.ContextSet.is_empty (snd body));