diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fa6422cdc5..8acc3c233a 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -170,7 +170,7 @@ module Make(T : Task) = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init 10 (fun _ -> + CList.init n (fun _ -> Universes.new_univ_level (Global.current_dirpath ())) in let rec kill_if () = diff --git a/stm/stm.ml b/stm/stm.ml index b4331dc460..f577994ffa 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2584,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; |