diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cc2c37790f..605f11d673 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -697,6 +697,14 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; *) (***********************************************************************) +(* Scrape *) + +let rec scrape_mind env kn = + match (Environ.lookup_mind kn env).mind_equiv with + | None -> kn + | Some kn' -> scrape_mind env kn' + +(***********************************************************************) (* Co-fixpoints. *) exception CoFixGuardError of guard_error |