diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-28 20:44:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-28 20:44:17 +0200 |
| commit | a6ea8b53198fbe6cc1740f8cc84c02b277b1d2ac (patch) | |
| tree | 527618196791526fd322dab327dd0c2222ecee04 /pretyping/inductiveops.ml | |
| parent | 15780e0ff875b6d8f336881021035464bd506eaf (diff) | |
Quick fix of bug #2996 continued (case of inductive types).
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 6fa93484f..07a337836 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -24,13 +24,15 @@ open Inductive Inductive, but they expect an env *) let type_of_inductive env (ind,u) = - let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive env (specif,u) + let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in + Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps; + Inductive.type_of_inductive env (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = - let specif = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let (mib,_ as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif let type_of_constructor_in_ctx env cstr = |