From 888d4be3ea2a45cff416fd8896276cfa8fc00518 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 10 Feb 2017 11:07:10 +0100
Subject: Make Obligations see fix_exn

---
 stm/stm.ml             |  1 +
 vernac/obligations.ml  | 12 ++++--------
 vernac/obligations.mli |  6 ++++++
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index fd1cefa8d..e698d1c72 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2961,5 +2961,6 @@ let parse_error_hook = Hooks.parse_error_hook
 let forward_feedback_hook = Hooks.forward_feedback_hook
 let process_error_hook = Hooks.process_error_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
+let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
 let tactic_being_run_hook = Hooks.tactic_being_run_hook
 (* vim:set foldmethod=marker: *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c1d9ae48a..6f3921903 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,17 +20,13 @@ open Pp
 open CErrors
 open Util
 
-(* EJGA: This should go away, no more need for fix_exn  *)
-module Stm = struct
-    let u = (fun x -> x)
-    let get_fix_exn () = u
-end
-
 module NamedDecl = Context.Named.Declaration
 
 let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
+let get_fix_exn, stm_get_fix_exn = Hook.make ()
+
 let succfix (depth, fixrels) =
   (succ depth, List.map succ fixrels)
 
@@ -491,7 +487,7 @@ let declare_definition prg =
   let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
-  let fix_exn = Stm.get_fix_exn () in
+  let fix_exn = Hook.get get_fix_exn () in
   let pl, ctx =
     Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
   let ce =
@@ -572,7 +568,7 @@ let declare_mutual_definition l =
   in
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
-  let fix_exn = Stm.get_fix_exn () in
+  let fix_exn = Hook.get get_fix_exn () in
   let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 80b689144..11366fe91 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -24,6 +24,12 @@ val declare_definition_ref :
      Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference Lemmas.declaration_hook -> global_reference) ref
 
+(* 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) Hook.t
+
+
 val check_evars : env -> evar_map -> unit
 
 val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
-- 
cgit v1.2.3