From dcf4d3e28813e09fc71f974b79ddf42d2e525976 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 5 Jun 2016 21:50:22 +0200
Subject: Remove the syntax changes introduced by this branch.

We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
---
 intf/vernacexpr.mli | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2f2f973761..d7b269a1de 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,14 +303,10 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * simple_binder with_coercion list
-  | VernacInductive of
-      bool (*[false] => assume positive*) *
-      private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
-      Declarations.typing_flags *
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-      Declarations.typing_flags *
       locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
-- 
cgit v1.2.3