diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ab2177f75..e3b152aae 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -256,6 +256,16 @@ let type_case_branches env (ind,largs) pj c = (************************************************************************) (* Checking the case annotation is relevent *) +let rec inductive_kn_equiv env kn1 kn2 = + match (lookup_mind kn1 env).mind_equiv with + | Some kn1' -> inductive_kn_equiv env kn2 kn1' + | None -> match (lookup_mind kn2 env).mind_equiv with + | Some kn2' -> inductive_kn_equiv env kn2' kn1 + | None -> false + +let inductive_equiv env (kn1,i1) (kn2,i2) = + i1=i2 & inductive_kn_equiv env kn1 kn2 + let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if |