From c4f800a1c92c7f558cdcb1915649e2666b1a897e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 30 Jun 2019 19:47:04 +0200
Subject: [vernac] Refactor Vernacular Control Attributes into a list

We place control attributes on their own, datatype, similarly to
regular attributes.

This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.
---
 plugins/funind/g_indfun.mlg             | 2 +-
 plugins/funind/glob_term_to_relation.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index d220058120..92a93489f4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -180,7 +180,7 @@ let is_proof_termination_interactively_checked recsl =
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
+    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacFixpoint(NoDischarge, List.map snd recsl)}))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 798c62d549..6eb8c42d1d 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 Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,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 Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)))
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
-- 
cgit v1.2.3