diff options
| author | Maxime Dénès | 2017-11-23 10:47:07 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 10:47:07 +0100 |
| commit | 22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (patch) | |
| tree | be15728b7f3925410fc07b36eef89ddc3fc9094c | |
| parent | 4768cad285711fd99fa6e15134cf20aefe78274e (diff) | |
| parent | b70cb4e567ff4917aff54f052f666374e6b3651d (diff) | |
Merge PR #6200: Remove pidentref grammar entry.
| -rw-r--r-- | API/API.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 1 insertions, 7 deletions
diff --git a/API/API.mli b/API/API.mli index 86c6f14158..a043a802ab 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4953,7 +4953,6 @@ sig val ident : Id.t Gram.entry val name : Name.t located Gram.entry val identref : Id.t located Gram.entry - val pidentref : (Id.t located * (Id.t located list) option) Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry val base_ident : Id.t Gram.entry diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 82306bb9f5..a01ea26af2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -132,7 +132,7 @@ let test_plural_form_types loc kwd = function (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition pidentref ident_decl; + record_field decl_notation rec_definition ident_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -222,9 +222,6 @@ GEXTEND Gram [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; r = universe_level -> (l, ord, r) ] ] ; - pidentref: - [ [ i = identref; l = OPT [ "@{" ; l = LIST0 identref; "}" -> l ] -> (i,l) ] ] - ; univ_decl : [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ]; cs = [ "|"; l' = LIST0 univ_constraint SEP ","; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index d34da159ee..8e6a01aa3b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -444,7 +444,6 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" - let pidentref = Gram.entry_create "Prim.pidentref" let ident_decl = Gram.entry_create "Prim.ident_decl" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2f03754193..d17ccb0b41 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -194,7 +194,6 @@ module Prim : val ident : Id.t Gram.entry val name : Name.t located Gram.entry val identref : Id.t located Gram.entry - val pidentref : (Id.t located * (Id.t located list) option) Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : Id.t located Gram.entry |