From 2f48ebef673d87cb29f29b0967c34357c8aea9cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 11:32:45 +0000
Subject: Commentaire

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3e2f03871a..545b5b83a1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -416,7 +416,7 @@ let inductive_of_fix env recarg body =
    subterm_specif env c ind 
 
    subterm_specif should test if [c] (building objects of inductive
-   type [ind], not necassarily the same as that of the recursive
+   type [ind], not necessarily the same as that of the recursive
    argument) is a subterm of the recursive argument of the fixpoint we
    are checking and fails with Not_found if not. In case it is, it
    should send its recursive specification (i.e. on which arguments we
-- 
cgit v1.2.3