diff options
Diffstat (limited to 'pretyping/namegen.mli')
| -rw-r--r-- | pretyping/namegen.mli | 42 |
1 files changed, 24 insertions, 18 deletions
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index f99ee3f6..637cbf64 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -1,19 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *) - open Names open Term open Environ -(**********************************************************************) -(* Generating "intuitive" names from their type *) +(********************************************************************* + Generating "intuitive" names from their type *) val lowercase_first_char : identifier -> string val sort_hdchar : sorts -> string @@ -24,7 +22,7 @@ val named_hd : env -> types -> name -> name val mkProd_name : env -> name * types * types -> types val mkLambda_name : env -> name * types * constr -> constr -(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) +(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) val prod_name : env -> name * types * types -> types val lambda_name : env -> name * types * constr -> constr @@ -38,32 +36,40 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr -(**********************************************************************) -(* Fresh names *) +(********************************************************************* + Fresh names *) + +(** Avoid clashing with a name satisfying some predicate *) +val next_ident_away_from : identifier -> (identifier -> bool) -> identifier -(* Avoid clashing with a name of the given list *) +(** Avoid clashing with a name of the given list *) val next_ident_away : identifier -> identifier list -> identifier -(* Avoid clashing with a name already used in current module *) +(** Avoid clashing with a name already used in current module *) val next_ident_away_in_goal : identifier -> identifier list -> identifier -(* Avoid clashing with a name already used in current module *) -(* but tolerate overwriting section variables, as in goals *) +(** Avoid clashing with a name already used in current module + but tolerate overwriting section variables, as in goals *) val next_global_ident_away : identifier -> identifier list -> identifier -(* Avoid clashing with a constructor name already used in current module *) +(** Avoid clashing with a constructor name already used in current module *) val next_name_away_in_cases_pattern : name -> identifier list -> identifier -val next_name_away : name -> identifier list -> identifier (* default is "H" *) +val next_name_away : name -> identifier list -> identifier (** default is "H" *) val next_name_away_with_default : string -> name -> identifier list -> identifier -(**********************************************************************) -(* Making name distinct for displaying *) +val next_name_away_with_default_using_types : string -> name -> + identifier list -> types -> identifier + +val set_reserved_typed_name : (types -> name) -> unit + +(********************************************************************* + Making name distinct for displaying *) type renaming_flags = - | RenamingForCasesPattern (* avoid only global constructors *) - | RenamingForGoal (* avoid all globals (as in intro) *) + | RenamingForCasesPattern (** avoid only global constructors *) + | RenamingForGoal (** avoid all globals (as in intro) *) | RenamingElsewhereFor of constr val make_all_name_different : env -> env |