From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- stm/vernac_classifier.ml | 24 ++++++++++++++---------- 1 file changed, 14 insertions(+), 10 deletions(-) (limited to 'stm/vernac_classifier.ml') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 783ff2e1..a898c687 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -86,7 +86,7 @@ let rec classify_vernac e = make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e -> classify_vernac_list e + | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ @@ -116,36 +116,36 @@ let rec classify_vernac e = | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ( - (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) -> + (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater - | VernacDefinition (_,(_,i),ProveBody _) -> + | VernacDefinition (_,((_,i),_),ProveBody _) -> VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater | VernacStartTheoremProof (_,l,_) -> let ids = - CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in + CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater | VernacFixpoint (_,l) -> let ids, open_proof = - List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> + List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (_,l) -> let ids, open_proof = - List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> + List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in + 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 + | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater | VernacInductive (_,_,l) -> - let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with + 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] | _ -> []) @ CList.map_filter (function @@ -173,9 +173,13 @@ let rec classify_vernac e = | VernacDeclareReduction _ | VernacDeclareClass _ | VernacDeclareInstances _ | VernacRegister _ - | VernacDeclareTacticDefinition _ | VernacNameSectionHypSet _ | VernacComments _ -> VtSideff [], VtLater + | VernacDeclareTacticDefinition (_,l) -> + let open Libnames in + VtSideff (List.map (function + | (Ident (_,r),_,_) -> r + | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow (* (Local) Notations have to disappear *) -- cgit v1.2.3