diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-22 16:55:44 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-22 16:55:44 +0000 |
commit | cf59b39d44a7a765d51b0a426ad6d71678740195 (patch) | |
tree | 4d6d5deff049574d40770c15feeef785dd2f5f07 /kernel/inductive.ml | |
parent | a96aa78636b5fb4ede593b02b1efa2d3025d65d9 (diff) |
module Wcclausenv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@130 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r-- | kernel/inductive.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 429d626f1..0154aa7a9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -50,6 +50,19 @@ let mis_recargs mis = let mis_recarg mis = mis.mis_mip.mind_listrec let mis_typename mis = mis.mis_mip.mind_typename +let is_recursive listind = + let rec one_is_rec rvec = + List.exists (function + | Mrec(i) -> List.mem i listind + | Imbr(_,_,lvec) -> one_is_rec lvec + | Norec -> false + | Param(_) -> false) rvec + in + array_exists one_is_rec + +let mis_is_recursive mis = + is_recursive (interval 0 ((mis_ntypes mis)-1)) (mis_recarg mis) + let mind_nth_type_packet mib n = mib.mind_packets.(n) (*s Declaration. *) |