From ccbe5c840923bc9b1a5965f5738c180410ea1df9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 13:08:32 +0000 Subject: [PATCH] fixed list.nth and added some paretheses --- helm/software/components/ng_kernel/nCicPp.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 27c7fc97e..087e58c98 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -14,16 +14,17 @@ module R = NReference let trivial_pp_term ~context ~subst ~metasenv = let rec aux ctx = function | C.Rel m -> - (try List.nth ctx m - with Not_found -> " -" ^ string_of_int (m - List.length context)) + (try List.nth ctx (m-1) + with Failure _ -> " -" ^ string_of_int (m - List.length context)) | C.Const r -> R.string_of_reference r - | C.Prod (name,s,t) -> " \Pi "^name^":"^aux ctx s^"."^aux (name::ctx) t - | C.Lambda (name,s,t) -> " \lambda "^name^":"^aux ctx s^"."^aux (name::ctx) t + | C.Prod (name,s,t) -> "(\Pi "^name^":"^aux ctx s^"."^aux (name::ctx) t^")" + | C.Lambda (name,s,t) -> + "(\lambda "^name^":"^aux ctx s^"."^aux (name::ctx) t^")" | C.LetIn (name,ty,t,b) -> - " let "^name^":"^aux ctx ty^":="^aux ctx t^" in "^aux (name::ctx) b + "(let "^name^":"^aux ctx ty^":="^aux ctx t^" in "^aux (name::ctx) b^")" | C.Match (_,oty,t,pl) -> - " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ "[" ^ - String.concat "|" (List.map (aux ctx) pl) ^ "]" + " match " ^ aux ctx t ^ " return " ^ aux ctx oty ^ "[" ^ + String.concat "|" (List.map (aux ctx) pl) ^ "]" | C.Appl l -> "("^String.concat " " (List.map (aux ctx) l) ^")" | C.Implicit _ -> "?" | C.Meta (n,_) -> "?"^string_of_int n -- 2.39.2