Do not refresh the names of implicit arguments.

Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)

This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.

Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.

The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.

Closes #6785
Closes #12001

Another step towards checking the standard library with `-mangle-names`.

1 files changed, 10 insertions, 20 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index db102470b0..48961c6c8a 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
 open Libobject
 open EConstr
 open Reductionops
-open Namegen
 open Constrexpr
 
 module NamedDecl = Context.Named.Declaration
@@ -247,24 +246,15 @@ let is_rigid env sigma t =
      is_rigid_head sigma t
   | _ -> true
 
-let find_displayed_name_in sigma all avoid na (env, b) =
-  let envnames_b = (env, b) in
-  let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in sigma flag avoid na b
-  else compute_displayed_name_in sigma flag avoid na b
-
-let compute_implicits_names_gen all env sigma t =
+let compute_implicits_names env sigma t =
   let open Context.Rel.Declaration in
-  let rec aux env avoid names t =
+  let rec aux env names t =
     let t = whd_all env sigma t in
     match kind sigma t with
     | Prod (na,a,b) ->
-       let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in
-       aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+       aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b
     | _ -> List.rev names
-  in aux env Id.Set.empty [] t
-
-let compute_implicits_names = compute_implicits_names_gen true
+  in aux env [] t
 
 let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
   let open Context.Rel.Declaration in
@@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t =
     (f.strict || f.strongly_strict) f.strongly_strict
     f.reversible_pattern f.contextual env sigma t
 
-let compute_implicits_flags env sigma f all t =
+let compute_implicits_flags env sigma f t =
   List.combine
-    (compute_implicits_names_gen all env sigma t)
+    (compute_implicits_names env sigma t)
     (compute_implicits_explanation_flags env sigma f t)
 
 let compute_auto_implicits env sigma flags enriching t =
@@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) =
 
 let rec prepare_implicits i f = function
   | [] -> []
-  | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
-  | (Name id, Some imp)::imps ->
+  | (na, Some imp)::imps ->
       let imps' = prepare_implicits (i+1) f imps in
-      Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps'
+      let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in
+      Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits (i+1) f imps
 
 let set_manual_implicits silent flags enriching autoimps l =
@@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l =
 
 let compute_semi_auto_implicits env sigma f t =
   if not f.auto then [DefaultImpArgs, []]
-  else let l = compute_implicits_flags env sigma f false t in
+  else let l = compute_implicits_flags env sigma f t in
        [DefaultImpArgs, prepare_implicits 1 f l]
 
 (*s Constants. *)