diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-02-10 11:07:10 +0100 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-15 20:45:29 +0100 |
| commit | 888d4be3ea2a45cff416fd8896276cfa8fc00518 (patch) | |
| tree | cdf0c5a856e29a9924a08fc961b29f6e59c56d45 /stm | |
| parent | 4db82417bdda1f9b0c7ea6ba9f6d71c03cc07eba (diff) | |
Make Obligations see fix_exn
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 1 |
1 files changed, 1 insertions, 0 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: *) |