diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 5 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index a79bf54267..8ca50e2d54 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -931,7 +931,7 @@ let show_script ?proof () = try let prf = try match proof with - | None -> Some (Pfedit.get_current_proof_name ()) + | None -> Some (Proof_global.get_current_proof_name ()) | Some (p,_) -> Some (p.Proof_global.id) with Proof_global.NoCurrentProof -> None in @@ -2046,7 +2046,8 @@ let collect_proof keep cur hd brkind id = | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in let check_policy rc = if async_policy () then rc else make_sync `Policy rc in match cur, (VCS.visit id).step, brkind with - | (parent, { expr = VernacExactProof _ }), `Fork _, _ -> + | (parent, { expr = VernacExactProof _ }), `Fork _, _ + | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> `Sync (no_name,None,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e458..87d9e411a7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -142,7 +142,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in VtSideff ids, VtLater | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> + | VernacInductive (_, _,_,l) -> let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ |