Make detyping robust w.r.t. indexed anonymous variables

I don't think there's a reason to treat such variables more severely
than unbound variables. This anomaly is often raised by debug printers
(e.g. when studying complex scenarios using `Set Unification Debug`),
and so makes debugging less convenient.

Fixes #3754, fixes #10026.

5 files changed, 12 insertions, 12 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 816316487c..2cd8cc3a74 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,7 +27,6 @@ open Clenv
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
 
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 062e3ca8b2..82726eccf0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable."))
-let set_detype_anonymous f = detype_anonymous := f
-
 let detype_level sigma l =
   let l = hack_qualid_of_univ_level sigma l in
   GType (UNamed l)
@@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t =
   match EConstr.kind sigma (collapse_appl sigma t) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
-	 | Name id   -> GVar id
-	 | Anonymous -> GVar (!detype_anonymous n)
+         | Name id   -> GVar id
+         | Anonymous ->
+           let s = "_ANONYMOUS_REL_"^(string_of_int n) in
+           GVar (Id.of_string s)
        with Not_found ->
-	 let s = "_UNBOUND_REL_"^(string_of_int n)
-	 in GVar (Id.of_string s))
+         let s = "_UNBOUND_REL_"^(string_of_int n)
+         in GVar (Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
         if n = Constr_matching.special_meta then
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 1a8e97efb8..00b0578a52 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo
 val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 
-(* XXX: This is a hack and should go away *)
-val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit
-
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v
new file mode 100644
index 0000000000..0d3142d0f2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10026.v
@@ -0,0 +1,3 @@
+Require Import Coq.Lists.List.
+Set Debug RAKAM.
+Check fun _ => fold_right (fun A B => prod A B) unit _.
diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v
index 18820b1a4c..7031cbf132 100644
--- a/test-suite/bugs/opened/bug_3754.v
+++ b/test-suite/bugs/closed/bug_3754.v
@@ -281,5 +281,7 @@ Defined.
                                  (factor2 fact)).
       rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
       Set Debug Tactic Unification.
-      Fail rewrite (concat_Ap ff2).
+      rewrite (concat_Ap ff2).
     Abort.
+
+End Factorization.