diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 56dcda6a4..f2855d508 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2254,7 +2254,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); + let opacity_of_produced_term = + match x.expr with + | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | _ -> Doesn'tGuaranteeOpacity in + VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin |