diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /library/nameops.mli |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'library/nameops.mli')
-rw-r--r-- | library/nameops.mli | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/library/nameops.mli b/library/nameops.mli new file mode 100644 index 00000000..4b7cecda --- /dev/null +++ b/library/nameops.mli @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: nameops.mli,v 1.12.2.1 2004/07/16 19:30:36 herbelin Exp $ *) + +open Names + +(* Identifiers and names *) +val pr_id : identifier -> Pp.std_ppcmds +val wildcard : identifier + +val make_ident : string -> int option -> identifier +val repr_ident : identifier -> string * int option + +val atompart_of_id : identifier -> string (* remove trailing digits *) +val root_of_id : identifier -> identifier (* remove trailing digits, ' and _ *) + +val add_suffix : identifier -> string -> identifier +val add_prefix : string -> identifier -> identifier + +val lift_ident : identifier -> identifier +val next_ident_away : identifier -> identifier list -> identifier +val next_ident_away_from : identifier -> identifier list -> identifier + +val next_name_away : name -> identifier list -> identifier +val next_name_away_with_default : + string -> name -> identifier list -> identifier + +val out_name : name -> identifier + +val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a +val name_cons : name -> identifier list -> identifier list +val name_app : (identifier -> identifier) -> name -> name + +val pr_lab : label -> Pp.std_ppcmds + +(* some preset paths *) + +val default_library : dir_path + +(* This is the root of the standard library of Coq *) +val coq_root : module_ident + +(* This is the default root prefix for developments which doesn't + mention a root *) +val default_root_prefix : dir_path + +(* Metavariables *) +val pr_meta : Term.metavariable -> Pp.std_ppcmds +val string_of_meta : Term.metavariable -> string |