diff options
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 7e394da2ed..6a99f201f3 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -196,12 +196,10 @@ struct (** Return a new rel-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx - (** Return the number of {e local declarations} in a given context. *) + (** Return the number of {e local declarations} in a given rel-context. *) let length = List.length - (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] - with n = |Δ| and with the local definitions of [Γ] skipped in - [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + (** Return the number of {e local assumptions} in a given rel-context. *) let nhyps ctx = let open Declaration in let rec nhyps acc = function @@ -413,7 +411,7 @@ struct (** empty named-context *) let empty = [] - (** empty named-context *) + (** Return a new named-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx (** Return the number of {e local declarations} in a given named-context. *) |