From 3af570b60e6912d2eb906ce86a3df3b8ecca675c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 12 Feb 2020 13:54:14 +0100
Subject: Don't duplicate the inductive keyword for each block elt when parsing

---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c5b3e0931b..65ef2ca8c6 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -131,7 +131,7 @@ let classify_vernac e =
         VtSideff ([id.CAst.v], VtLater)
     | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
     | VernacInductive (_, _,_,l) ->
-        let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
+        let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
-- 
cgit v1.2.3