diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-04 18:51:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-24 11:14:13 +0200 |
| commit | 341dcf85e43bd2569910426cfbcdc28032dfdb68 (patch) | |
| tree | cea15d9b1b91443b371b866dc2d47e064a8e9920 /kernel/context.ml | |
| parent | 0897d0f642c19419c513f9609782436bebf28f5b (diff) | |
A missing newline after a comment.
Diffstat (limited to 'kernel/context.ml')
| -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 |