diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c70..4cc362ddab 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 diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2b5eb86834..03ade646b2 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -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] | _ -> []) @ |