diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 11:32:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 11:32:45 +0000 |
| commit | 2f48ebef673d87cb29f29b0967c34357c8aea9cd (patch) | |
| tree | 60ff5b1540389c4326f06c372e157fe8737f6fd4 /kernel | |
| parent | f39cd683cb022d877a0d2ebd014fa0879bc6de00 (diff) | |
Commentaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6409 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3e2f03871..545b5b83a 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 |