From de7d2fdb97975dcd94005bb6fa79a312c8afa017 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 28 Oct 2017 20:07:44 +0200 Subject: Fixing #5401 (printing of patterns with bound anonymous variables). This fixes also #5731, #6035, #5364. --- engine/namegen.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'engine/namegen.ml') diff --git a/engine/namegen.ml b/engine/namegen.ml index 2e62b8901..a38c73ed0 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -376,15 +376,22 @@ let next_name_for_display sigma flags = | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in sigma flags avoid na c = +let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c = match na with - | Anonymous when noccurn sigma 1 c -> + | Anonymous when noccurn_fun sigma 1 c -> (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in + let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in (idopt, Id.Set.add fresh_id avoid) +let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn + +let compute_displayed_name_in_gen f sigma = + (* only flag which does not need a constr, maybe to be refined *) + let flag = RenamingForGoal in + compute_displayed_name_in_gen_poly f sigma flag + let compute_and_force_displayed_name_in sigma flags avoid na c = match na with | Anonymous when noccurn sigma 1 c -> -- cgit v1.2.3