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.
---
 dev/top_printers.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

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