diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-11 12:25:59 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-11 12:50:06 +0200 |
| commit | efca6e2f2268a6ff0a7c06ff28fffd02243f02c1 (patch) | |
| tree | 592f9faf6da6e51a4641baa2b3f7fe4ae1e5be24 /engine/namegen.ml | |
| parent | d8a07b44f5245f8e2f3a47095c70bb3cc85e3d99 (diff) | |
CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function
Diffstat (limited to 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |