From 3960836e255e3738cabcd559cc1c133c5f30137a Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Tue, 16 Feb 2016 11:46:37 +0100
Subject: Term: fix a comment (first de Bruijn index is 1)

---
 kernel/term.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 7f79f6403..32267f6c4 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -202,7 +202,7 @@ val destCoFix : constr -> cofixpoint
 
 (** non-dependent product [t1 -> t2], an alias for
    [forall (_:t1), t2]. Beware [t_2] is NOT lifted.
-   Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))]
+   Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 1) (mkRel 2))]
 *)
 val mkArrow : types -> types -> constr
 
-- 
cgit v1.2.3