diff options
| author | herbelin | 2000-10-11 13:41:26 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-11 13:41:26 +0000 |
| commit | 9ca14acd5acdd6159540d072a777adb4b9ed5ed0 (patch) | |
| tree | e8b5a84f915e575aa150ddc1b52a55a89f4d4609 /kernel/typeops.ml | |
| parent | d510a00bbe0223a34e1fe2f8ad77f9141ec700e2 (diff) | |
Prise en compte de Let dans build_dependent_inductive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8421a05434..5aaa47847d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -166,7 +166,7 @@ in let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = let kelim = mis_kelim mis in let arsign,s = get_arity indf in - let glob_t = prod_it (mkSort s) arsign in + let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in dep |