diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-21 00:03:37 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-03-21 00:03:37 +0000 |
commit | 73e027a781c1025914749975d341dbab21e2bc45 (patch) | |
tree | 588e9ef6035cd7d48346e9dba7ab15c1e4490fef /kernel/indtypes.ml | |
parent | 1c1b6f2da919c1303b87b97119b621a06952fadc (diff) |
Prise en compte nouveau case_info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@334 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r-- | kernel/indtypes.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 359f92d4b..ab7263503 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -23,15 +23,6 @@ let mind_check_arities env mie = in List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds -let sort_of_arity env c = - let rec sort_of ar = - match whd_betadeltaiota env Evd.empty ar with - | DOP0 (Sort s) -> s - | DOP2 (Prod, _, DLAM (_, c)) -> sort_of c - | _ -> error "not an arity" - in - sort_of c - let allowed_sorts issmall isunit = function | Type _ -> [prop;spec;types] @@ -224,10 +215,12 @@ let cci_inductive env env_ar kind nparams finite inds cst = let one_packet i (id,ar,cnames,issmall,isunit,lc) = let recargs = listrec_mconstr env_ar ntypes nparams i lc in let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in - let kelim = allowed_sorts issmall isunit (sort_of_arity env ar.body) in + let (ar_sign,ar_sort) = splay_arity env Evd.empty ar.body in + let kelim = allowed_sorts issmall isunit ar_sort in { mind_consnames = Array.of_list cnames; mind_typename = id; mind_lc = lc; + mind_nrealargs = List.length ar_sign - nparams; mind_arity = ar; mind_kelim = kelim; mind_listrec = recargs; |