From 3e460f77c1777ce1a8d393f2335fd7f4b4fe924f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Feb 2020 12:35:27 +0100
Subject: Fixing wrong comments in context.ml.

---
 kernel/context.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'kernel/context.ml')

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. *)
-- 
cgit v1.2.3