From 9615c025a2a09b69f2001d44a66a1fddef74e680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 29 Sep 2016 15:51:18 +0200
Subject: Fix bug #4869, allow Prop, Set, and level names in constraints.

---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/vernacexpr.mli')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed44704df4..e6599a30d1 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -346,7 +346,7 @@ type vernac_expr =
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
-  | VernacConstraint of (lident * Univ.constraint_type * lident) list
+  | VernacConstraint of (glob_level * Univ.constraint_type * glob_level) list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident
-- 
cgit v1.2.3


From 601fd9343a241706c0a205aaf8e08255753c3780 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 29 Sep 2016 15:23:07 +0200
Subject: Arguments: cleanup + detect discrepancy rename/implicit (#3753)

It seems warnings are not taken into account in output/
tests.
---
 intf/vernacexpr.mli | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'intf/vernacexpr.mli')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ed44704df4..6df85f0764 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -415,7 +415,7 @@ type vernac_expr =
   | VernacDeclareImplicits of reference or_by_notation *
       (explicitation * bool * bool) list list
   | VernacArguments of reference or_by_notation *
-      ((Name.t * bool * (Loc.t * string) option * bool * bool) list) list *
+      (vernac_argument_status list) list *
       int * [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
               `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
               `DefaultImplicits ] list
@@ -477,6 +477,13 @@ and tacdef_body =
   | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
   | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
 
+and vernac_argument_status = {
+  name : Name.t;
+  recarg_like : bool;
+  notation_scope : (Loc.t * string) option;
+  implicit_status : [ `Implicit | `MaximallyImplicit | `NotImplicit];
+}
+
 (* A vernac classifier has to tell if a command:
    vernac_when: has to be executed now (alters the parser) or later
    vernac_type: if it is starts, ends, continues a proof or
-- 
cgit v1.2.3


From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Sep 2016 17:15:10 +0200
Subject: Fix bug #4798: compat notations should not modify the parser.

This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
---
 intf/vernacexpr.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'intf/vernacexpr.mli')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 6df85f0764..1063a74d9f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -211,8 +211,9 @@ type syntax_modifier =
   | SetLevel of int
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
-  | SetOnlyParsing of Flags.compat_version
+  | SetOnlyParsing
   | SetOnlyPrinting
+  | SetCompatVersion of Flags.compat_version
   | SetFormat of string * string located
 
 type proof_end =
-- 
cgit v1.2.3