diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 177a76e64b..04f08e488b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1684,7 +1684,9 @@ end = struct (* {{{ *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); - `OK proof + (* Is this name the same than the one in scope? *) + let name = Declare.get_po_name proof in + `OK name end with e -> let (e, info) = Exninfo.capture e in @@ -1723,7 +1725,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK { Declare.name } -> + | `OK name -> let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with |