diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 6 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4f014be2d..9edc1f1c7 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_,_, _, iednll) -> + | VernacInductive (_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin @@ -598,14 +598,14 @@ let rec tmpp v loc = (fun (ie, dnl) -> (pp_inductive_expr ie) @ (List.map pp_decl_notation dnl)) iednll) in xmlInductive kind loc exprs - | VernacFixpoint (_,_, fednll) -> + | VernacFixpoint (_, fednll) -> let exprs = List.flatten (* should probably not be flattened *) (List.map (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ (List.map pp_decl_notation dnl)) fednll) in xmlFixpoint exprs - | VernacCoFixpoint (_,_, cfednll) -> + | VernacCoFixpoint (_, cfednll) -> (* Nota: it is like VernacFixpoint without so could be merged *) let exprs = List.flatten (* should probably not be flattened *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 574cc0044..2b5eb8683 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -125,14 +125,14 @@ let rec classify_vernac e = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,_,l) -> + | VernacFixpoint (_,l) -> let ids, open_proof = 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) -> + | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd 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] | _ -> []) @ |