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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 274bfc33c..4df08b6a1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -135,7 +135,7 @@ let make_cases s = let rec rename avoid = function | [] -> [] | (n,_)::l -> - let n' = Namegen.next_name_away_in_cases_pattern n avoid in + let n' = Namegen.next_name_away_in_cases_pattern ([],mkMeta 0) n avoid in Id.to_string n' :: rename (n'::avoid) l in let al' = rename [] al in (Id.to_string consname :: al') :: l) |