From 28d38568e437a09fe3835e2644c4e420dbc4ba51 Mon Sep 17 00:00:00 2001
From: clrenard
Date: Mon, 23 Jul 2001 08:31:44 +0000
Subject: Comentaire errone.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1863 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 e81791426f..8a5a402a74 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -540,7 +540,7 @@ val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr
 val subst_term_occ_decl : occs:int list -> what:constr ->
       where:named_declaration -> named_declaration
 
-(* [replace_subst_term c by_c in_t substitutes c by by_c in in_t *)
+(* [replace_term c by_c in_t substitutes c by by_c in in_t *)
 val replace_term : constr -> constr -> constr -> constr
 
 (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] 
-- 
cgit v1.2.3