diff options
| author | Gaëtan Gilbert | 2019-05-05 16:42:36 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 09:33:41 +0200 |
| commit | 33b18aaffd999fb6d31fd5e9c7ca4426d5186983 (patch) | |
| tree | 0b0f5efeb5e9cbe2fb3eabaff058e25cf4b5eac9 | |
| parent | 1bf2a088387949c13602997d181e6f7d0f014b3f (diff) | |
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)
| -rw-r--r-- | vernac/g_vernac.mlg | 3 |
1 files changed, 1 insertions, 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 *) |