From 33b18aaffd999fb6d31fd5e9c7ca4426d5186983 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 5 May 2019 16:42:36 +0200
Subject: instance_name grammar entry isn't global

Not needed since we don't allow anonymous Declare Instance
anymore (was needed for factorization or some such before that I think)
---
 vernac/g_vernac.mlg | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5eec8aed1e..63e6dd247f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -50,7 +50,6 @@ let def_body = Entry.create "vernac:def_body"
 let decl_notation = Entry.create "vernac:decl_notation"
 let record_field = Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
-let instance_name = Entry.create "vernac:instance_name"
 let section_subset_expr = Entry.create "vernac:section_subset_expr"
 
 let make_bullet s =
@@ -683,7 +682,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)
 GRAMMAR EXTEND Gram
-  GLOBAL: gallina_ext instance_name hint_info;
+  GLOBAL: gallina_ext hint_info;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
-- 
cgit v1.2.3