From 58ce236b589513e779e00759e54e72cbbf2bd2c3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Apr 2008 15:24:54 +0000 Subject: [PATCH] print unnamed variables as __n --- helm/software/components/ng_kernel/nCicPp.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 5a96545fe..a0f0a8afb 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -49,8 +49,10 @@ let trivial_pp_term ~context ~subst ~metasenv ?(inside_fix=false) t = let module F = Format in let rec aux ?(toplevel=false) ctx = function | C.Rel m -> - (try F.fprintf f "%s" (List.nth ctx (m-1)) - with Failure _ -> F.fprintf f " -%d" (m - List.length context)) + (try + let name = List.nth ctx (m-1) in + F.fprintf f "%s" (if name = "_" then "__"^string_of_int m else name) + with Failure _ -> F.fprintf f " -%d" (m - List.length context)) | C.Const r -> F.fprintf f "%s" (r2s inside_fix r) | C.Prod ("_",s,t) -> if not toplevel then F.fprintf f "("; -- 2.39.2