diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-21 13:45:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-07-21 13:45:23 +0000 |
| commit | 8fea90d232c75b23c0bfe1d4b4f136f6a6f5aee8 (patch) | |
| tree | 6b356d3c2c68eb4747f488926015c8fde2a4f649 /kernel | |
| parent | 488c6ae3e30385f49346c451d10401526d4cf358 (diff) | |
Utilisation de la non-équivalence d'inductifs pour le case_info (cf message CP et EC dans coqdev)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7250 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |