From 0324a38f142a82d591ab66ade61678f35b12bea4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 25 Aug 2014 20:21:06 +0200 Subject: 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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- toplevel/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') 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) -- cgit v1.2.3