aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--API/API.mli1
-rw-r--r--parsing/g_vernac.ml45
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli1
4 files changed, 1 insertions, 7 deletions
diff --git a/API/API.mli b/API/API.mli
index 86c6f1415..a043a802a 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 82306bb9f..a01ea26af 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 d34da159e..8e6a01aa3 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 2f0375419..d17ccb0b4 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