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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/context.mli')

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