Add functionality to permit printing terms with references to anonymous variables, useful for debugging

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9652 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 1 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 04665e282..a0071d5b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -358,12 +358,15 @@ let detype_sort = function
 (**********************************************************************)
 (* Main detyping function                                             *)
 
+let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable")
+let set_detype_anonymous f = detype_anonymous := f
+
 let rec detype (isgoal:bool) avoid env t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> RVar (dl, id)
-	 | Anonymous -> anomaly "detype: index to an anonymous variable"
+	 | Anonymous -> !detype_anonymous dl n
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
 	 in RVar (dl, id_of_string s))