From 9f834bd7ca7de79dfb2d9f9633ac93464ab1342d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 18:36:10 +0100
Subject: Make Cumulative, NonCumulative and Private attributes.

- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).

We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.
---
 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 15e839c612..567acb1c73 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -130,7 +130,7 @@ let classify_vernac e =
     | VernacPrimitive (id,_,_) ->
         VtSideff ([id.CAst.v], VtLater)
     | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
-    | VernacInductive (_, _,_,l) ->
+    | VernacInductive (_,l) ->
         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] | _ -> []) @
-- 
cgit v1.2.3