From efca6e2f2268a6ff0a7c06ff28fffd02243f02c1 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 11 Aug 2016 12:25:59 +0200 Subject: CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function --- engine/namegen.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'engine/namegen.ml') diff --git a/engine/namegen.ml b/engine/namegen.ml index bc04e3e48..8a766a717 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -114,9 +114,9 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env |> to_tuple with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) + try match Environ.lookup_rel (n-k) env with + | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id + | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> let id = match lna.(i) with Name id -> id | _ -> assert false in -- cgit v1.2.3