From cf9f4e566b87d2875f757bb7d54ee4421988e315 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 10 May 2019 12:32:07 +0200
Subject: 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.
---
 pretyping/detyping.ml  | 13 ++++++-------
 pretyping/detyping.mli |  3 ---
 2 files changed, 6 insertions(+), 10 deletions(-)

(limited to 'pretyping')

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
 
-- 
cgit v1.2.3