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.
---
 plugins/funind/glob_term_to_relation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c7dfe69fb1..e08ad9af3a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1517,7 +1517,7 @@ let do_build_inductive
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             msg
         in
@@ -1532,7 +1532,7 @@ let do_build_inductive
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             CErrors.print reraise
         in
-- 
cgit v1.2.3