From 4cdb838ef260c12f59cb91915c78dc975bd4c157 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 11 Dec 2017 16:17:39 +0000
Subject: [vernac] Define types in order

---
 intf/vernacexpr.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 5106e513b9..ba8dd41826 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -314,6 +314,15 @@ type cumulative_inductive_parsing_flag =
 
 (** {6 The type of vernacular expressions} *)
 
+type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
+
+type vernac_argument_status = {
+  name : Name.t;
+  recarg_like : bool;
+  notation_scope : string Loc.located option;
+  implicit_status : vernac_implicit_status;
+}
+
 type vernac_expr =
 
   | VernacLoad of verbose_flag * string
@@ -468,15 +477,6 @@ type vernac_expr =
   | VernacPolymorphic of bool * vernac_expr
   | VernacLocal of bool * vernac_expr
 
-and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
-and vernac_argument_status = {
-  name : Name.t;
-  recarg_like : bool;
-  notation_scope : string Loc.located option;
-  implicit_status : vernac_implicit_status;
-}
-
 type vernac_control =
   | VernacExpr of vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
-- 
cgit v1.2.3


From ab8e47207245277cb5b92b80a92ae78ede5bfafe Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 12 Dec 2017 15:32:59 +0000
Subject: [vernac] vernac_expr no longer recursive

---
 intf/vernacexpr.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index ba8dd41826..f35eab47fe 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -323,7 +323,7 @@ type vernac_argument_status = {
   implicit_status : vernac_implicit_status;
 }
 
-type vernac_expr =
+type nonrec vernac_expr =
 
   | VernacLoad of verbose_flag * string
   (* Syntax *)
@@ -472,13 +472,13 @@ type vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-  (* Flags *)
-  | VernacProgram of vernac_expr
-  | VernacPolymorphic of bool * vernac_expr
-  | VernacLocal of bool * vernac_expr
+type nonrec vernac_flag =
+  | VernacProgram
+  | VernacPolymorphic of bool
+  | VernacLocal of bool
 
 type vernac_control =
-  | VernacExpr of vernac_expr
+  | VernacExpr of vernac_flag list * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
   | VernacTime of bool * vernac_control located
-- 
cgit v1.2.3