diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-25 20:21:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-25 20:46:27 +0200 |
| commit | 0324a38f142a82d591ab66ade61678f35b12bea4 (patch) | |
| tree | c80868cc35333e7f900f528ba6cb353e0c6af6dc /pretyping/namegen.mli | |
| parent | aa2f0216bb39a1054737b1edf695f28f59c14ea7 (diff) | |
Fixing the essence of naming bug #3204: use same strategy for naming
cases pattern variables than for naming forall/fun binders (but still
avoiding constructor names).
Note in passing: such as it is implemented, the general strategy is in
O(n²) in the number of nested binders, because, when computing the
name for each 'fun x => c" (or forall, or a pattern name), the names
from the outside c and visibly occurring in c are computed.
Diffstat (limited to 'pretyping/namegen.mli')
| -rw-r--r-- | pretyping/namegen.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index 88ce43f8e..e1f55be6e 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -64,7 +64,7 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t val next_global_ident_away : Id.t -> Id.t list -> Id.t (** Avoid clashing with a constructor name already used in current module *) -val next_name_away_in_cases_pattern : Name.t -> Id.t list -> Id.t +val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t (** Default is [default_non_dependent_ident] *) val next_name_away : Name.t -> Id.t list -> Id.t @@ -81,7 +81,7 @@ val set_reserved_typed_name : (types -> Name.t) -> unit Making name distinct for displaying *) type renaming_flags = - | RenamingForCasesPattern (** avoid only global constructors *) + | RenamingForCasesPattern of (Name.t list * constr) (** avoid only global constructors *) | RenamingForGoal (** avoid all globals (as in intro) *) | RenamingElsewhereFor of (Name.t list * constr) |