diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index d1250331c3..6144f20cbd 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -83,4 +83,7 @@ val lookup_constant : constant -> env -> constant_body (* Mutual Inductives *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +(* Find the ultimate inductive in the [mind_equiv] chain *) +val scrape_mind : env -> mutual_inductive -> mutual_inductive + |