diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index c1156b9afe..5b88ee3d68 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1522,15 +1522,15 @@ end = struct (* {{{ *) let st = State.freeze () in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> - let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; let pobject, _info = - PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let st = Vernacstate.freeze_interp_state ~marshallable:false in + let opaque = Proof_global.Opaque in stm_qed_delay_proof ~st ~id:stop ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in ignore(Future.join checked_proof); @@ -2479,13 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ~drop_pt exn_info block_stop, ref false in qed.fproof <- Some (Some fp, cancel); - let opaque = match keep' with - | VtKeepAxiom | VtKeepOpaque -> - Proof_global.Opaque (* Admitted -> Opaque should be OK. *) - | VtKeepDefined -> Proof_global.Transparent + let () = match keep' with + | VtKeepAxiom | VtKeepOpaque -> () + | VtKeepDefined -> + CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.") in let proof, info = - PG_compat.close_future_proof ~opaque ~feedback_id:id fp in + PG_compat.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; let st = Vernacstate.freeze_interp_state ~marshallable:false in |