diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e9b504e05d..d1fd1edc78 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -159,25 +159,25 @@ module Prim : open Names open Libnames val preident : string Gram.entry - val ident : identifier Gram.entry + val ident : Id.t Gram.entry val name : name located Gram.entry - val identref : identifier located Gram.entry - val pattern_ident : identifier Gram.entry - val pattern_identref : identifier located Gram.entry - val base_ident : identifier Gram.entry + val identref : Id.t located Gram.entry + val pattern_ident : Id.t Gram.entry + val pattern_identref : Id.t located Gram.entry + val base_ident : Id.t Gram.entry val natural : int Gram.entry val bigint : Bigint.bigint Gram.entry val integer : int Gram.entry val string : string Gram.entry val qualid : qualid located Gram.entry - val fullyqualid : identifier list located Gram.entry + val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry val by_notation : (Loc.t * string * string option) Gram.entry val smart_global : reference or_by_notation Gram.entry val dirpath : dir_path Gram.entry val ne_string : string Gram.entry val ne_lstring : string located Gram.entry - val var : identifier located Gram.entry + val var : Id.t located Gram.entry end module Constr : @@ -187,7 +187,7 @@ module Constr : val lconstr : constr_expr Gram.entry val binder_constr : constr_expr Gram.entry val operconstr : constr_expr Gram.entry - val ident : identifier Gram.entry + val ident : Id.t Gram.entry val global : reference Gram.entry val sort : glob_sort Gram.entry val pattern : cases_pattern_expr Gram.entry @@ -197,7 +197,7 @@ module Constr : val binder : local_binder list Gram.entry (* closed_binder or variable *) val binders : local_binder list Gram.entry (* list of binder *) val open_binders : local_binder list Gram.entry - val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry + val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry val typeclass_constraint : (name located * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry val appl_arg : (constr_expr * explicitation located option) Gram.entry |