diff options
| -rw-r--r-- | kernel/context.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 929324efe..d635c4515 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -379,8 +379,9 @@ struct (** Return the number of {e local declarations} in a given named-context. *) let length = List.length -(** Return a declaration designated by a given de Bruijn index. - @raise Not_found if the designated identifier is not present in the designated named-context. *) let rec lookup id = function +(** Return a declaration designated by a given identifier + @raise Not_found if the designated identifier is not present in the designated named-context. *) + let rec lookup id = function | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl | _ :: sign -> lookup id sign | [] -> raise Not_found |