Merge PR #11550: Fixing wrong comments in context.ml

Reviewed-by: ppedrot

2 files changed, 4 insertions, 6 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 7e394da2ed..500ed20343 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -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. *)
diff --git a/kernel/context.mli b/kernel/context.mli
index 8f233613da..04aa039a01 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -129,7 +129,7 @@ sig
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
   val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
 
-  (** Return the number of {e local declarations} in a given context. *)
+  (** Return the number of {e local declarations} in a given rel-context. *)
   val length : ('c, 't) pt -> int
 
   (** Check whether given two rel-contexts are equal. *)