[declare] Remove some unused `fix_exn`

In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.

However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.

Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.

This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.

We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.

This has been tested in the case that tactics succeed but Qed fails
asynchronously.

2 files changed, 11 insertions, 39 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index e3144b2d24..59922c662a 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -140,9 +140,9 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
 
 (** [univsbody] are universe-constraints attached to the body-only,
    used in vio-delayed opaque constants and private poly universes *)
-let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
-  { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
+  { proof_entry_body = Future.from_val ((body,univsbody), eff);
     proof_entry_secctx = section_vars;
     proof_entry_type = types;
     proof_entry_universes = univs;
@@ -151,7 +151,7 @@ let definition_entry_core ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id
     proof_entry_inline_code = inline}
 
 let definition_entry =
-  definition_entry_core ?fix_exn:None ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
+  definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None
 
 type proof_object =
   { name : Names.Id.t
@@ -369,9 +369,9 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+let pure_definition_entry ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) body =
-  { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
+  { proof_entry_body = Future.from_val ((body,Univ.ContextSet.empty), ());
     proof_entry_secctx = None;
     proof_entry_type = types;
     proof_entry_universes = univs;
@@ -504,17 +504,6 @@ let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
   let () = register_constant kn kind local in
   kn
 
-let get_cd_fix_exn = function
-  | DefinitionEntry de ->
-    Future.fix_exn_of de.proof_entry_body
-  | _ -> fun x -> x
-
-let declare_constant ?local ~name ~kind cd =
-  try declare_constant ?local ~name ~kind cd
-  with exn ->
-    let exn = Exninfo.capture exn in
-    Exninfo.iraise (get_cd_fix_exn cd exn)
-
 let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
   let kn, eff =
     let de =
@@ -1010,29 +999,22 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in
   dref
 
-let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
-  try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
-  with exn ->
-    let exn = Exninfo.capture exn in
-    let exn = Option.cata (fun fix -> fix exn) exn fix_exn in
-    Exninfo.iraise exn
-
 (* Preparing proof entries *)
 
-let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
+let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma =
   let env = Global.env () in
   Pretyping.check_evars_are_solved ~program_mode:false env sigma;
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let entry = definition_entry_core ?fix_exn ?opaque ?inline ?types ~univs body in
+  let entry = definition_entry ?opaque ?inline ?types ~univs body in
   let uctx = Evd.evar_universe_context sigma in
   entry, uctx
 
 let declare_definition_core ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
-    ~obls ~poly ?inline ~types ~body ?fix_exn sigma =
-  let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+    ~obls ~poly ?inline ~types ~body sigma =
+  let entry, uctx = prepare_definition ~opaque ~poly ~udecl ~types ~body ?inline sigma in
   declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry
 
 let declare_definition = declare_definition_core ~obls:[]
@@ -1454,8 +1436,6 @@ let subst_prog subst prg =
     ( Vars.replace_vars subst' prg.prg_body
     , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type )
 
-let stm_get_fix_exn = ref (fun _ x -> x)
-
 let declare_definition prg =
   let varsubst = obligation_substitution true prg in
   let sigma = Evd.from_ctx prg.prg_ctx in
@@ -1471,12 +1451,11 @@ let declare_definition prg =
     , Decls.(IsDefinition prg.prg_kind)
     , prg.prg_implicits )
   in
-  let fix_exn = !stm_get_fix_exn () in
   let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
   (* XXX: This is doing normalization twice *)
   let kn =
     declare_definition_core ~name ~scope ~kind ~impargs ?hook ~obls
-      ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
+      ~opaque ~poly ~udecl ~types ~body sigma
   in
   let pm = progmap_remove !State.prg_ref prg in
   State.prg_ref := pm;
diff --git a/vernac/declare.mli b/vernac/declare.mli
index ef4f8c4825..979bdd4334 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -305,13 +305,11 @@ val declare_definition
   -> ?inline:bool
   -> types:EConstr.t option
   -> body:EConstr.t
-  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> Evd.evar_map
   -> GlobRef.t
 
 val declare_assumption
-  :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-  -> name:Id.t
+  :  name:Id.t
   -> scope:locality
   -> hook:Hook.t option
   -> impargs:Impargs.manual_implicits
@@ -495,11 +493,6 @@ val obl_substitution :
 
 val dependencies : Obligation.t array -> int -> Int.Set.t
 
-(* This is a hack to make it possible for Obligations to craft a Qed
- * behind the scenes.  The fix_exn the Stm attaches to the Future proof
- * is not available here, so we provide a side channel to get it *)
-val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref
-
 end
 
 (** Creating high-level proofs with an associated constant *)