diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 23d68c4b86..6f34c8dbc3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -896,6 +896,7 @@ end = struct (* {{{ *) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in + cur_id := Stateid.dummy; VCS.reached id; let ie = match Stateid.get info, safe_id with @@ -2583,12 +2584,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = - match x.expr with + let rec opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); + VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[])); let proof_mode = default_proof_mode () in VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode; |