diff options
Diffstat (limited to 'library/nameops.mli')
| -rw-r--r-- | library/nameops.mli | 47 |
1 files changed, 25 insertions, 22 deletions
diff --git a/library/nameops.mli b/library/nameops.mli index 9571d2a3..23432ae2 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,43 +9,46 @@ open Names (** Identifiers and names *) -val pr_id : identifier -> Pp.std_ppcmds -val pr_name : name -> Pp.std_ppcmds +val pr_id : Id.t -> Pp.std_ppcmds +val pr_name : Name.t -> Pp.std_ppcmds -val make_ident : string -> int option -> identifier -val repr_ident : identifier -> string * int option +val make_ident : string -> int option -> Id.t +val repr_ident : Id.t -> string * int option -val atompart_of_id : identifier -> string (** remove trailing digits *) -val root_of_id : identifier -> identifier (** remove trailing digits, ' and _ *) +val atompart_of_id : Id.t -> string (** remove trailing digits *) +val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) -val add_suffix : identifier -> string -> identifier -val add_prefix : string -> identifier -> identifier +val add_suffix : Id.t -> string -> Id.t +val add_prefix : string -> Id.t -> Id.t -val has_subscript : identifier -> bool -val lift_subscript : identifier -> identifier -val forget_subscript : identifier -> identifier +val has_subscript : Id.t -> bool +val lift_subscript : Id.t -> Id.t +val forget_subscript : Id.t -> Id.t -val out_name : name -> identifier +val out_name : Name.t -> Id.t +(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"] + otherwise. *) -val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a -val name_iter : (identifier -> unit) -> name -> unit -val name_cons : name -> identifier list -> identifier list -val name_app : (identifier -> identifier) -> name -> name -val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name +val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a +val name_iter : (Id.t -> unit) -> Name.t -> unit +val name_cons : Name.t -> Id.t list -> Id.t list +val name_app : (Id.t -> Id.t) -> Name.t -> Name.t +val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t -val pr_lab : label -> Pp.std_ppcmds +val pr_lab : Label.t -> Pp.std_ppcmds (** some preset paths *) -val default_library : dir_path +val default_library : DirPath.t (** This is the root of the standard library of Coq *) -val coq_root : module_ident +val coq_root : module_ident (** "Coq" *) +val coq_string : string (** "Coq" *) (** This is the default root prefix for developments which doesn't mention a root *) -val default_root_prefix : dir_path +val default_root_prefix : DirPath.t (** Metavariables *) val pr_meta : Term.metavariable -> Pp.std_ppcmds |