diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 28d5447c44..0216eef75f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1105,6 +1105,7 @@ module Backtrack : sig (* Returns the state that the command should backtract to *) val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option + val get_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1250,6 +1251,7 @@ end = struct (* {{{ *) end (* }}} *) let get_prev_proof = Backtrack.get_prev_proof +let get_proof = Backtrack.get_proof let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = |