From 85af5bb1ec5b2f080e267b8a8bb4438f8f640eb1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 9 Mar 2008 16:40:36 +0000
Subject: Fix a few bugs in Program: use user-given typing constraints for
 constant declarations, correct coercion between dependent products. Remove
 fragile inh_conv_coerces_to code, may break existing Programs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10647 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/term.mli b/kernel/term.mli
index 2c6e7f0b48..8d6c20a353 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -449,7 +449,7 @@ val noccur_with_meta : int -> int -> constr -> bool
 (* [exliftn el c] lifts [c] with lifting [el] *)
 val exliftn : Esubst.lift -> constr -> constr
 
-(* [liftn n k c] lifts by [n] indexes above [k] in [c] *)
+(* [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
 val liftn : int -> int -> constr -> constr
 
 (* [lift n c] lifts by [n] the positive indexes in [c] *)
-- 
cgit v1.2.3