From a6ea8b53198fbe6cc1740f8cc84c02b277b1d2ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 28 Jun 2014 20:44:17 +0200
Subject: Quick fix of bug #2996 continued (case of inductive types).

---
 pretyping/inductiveops.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6fa93484f5..07a3378363 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 =
-- 
cgit v1.2.3