diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /pretyping/namegen.mli | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
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 464efcf8..e23c6dad 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-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: namegen.mli 15069 2012-03-20 14:06:07Z 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 (name list * constr) val make_all_name_different : env -> env |