Change the place of inference after sect discharge

3 files changed, 29 insertions, 22 deletions

diff --git a/library/declare.ml b/library/declare.ml
index f3150174c..fcaadaa6e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -356,6 +356,21 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_private = None;
 })
 
+(* reinfer subtyping constraints for inductive after section is dischared. *)
+let infer_inductive_subtyping (pth, mind_ent) = 
+  if mind_ent.mind_entry_polymorphic then
+    begin
+      let env = Global.env () in
+      let env' =
+        Environ.push_context (Univ.UInfoInd.univ_context mind_ent.mind_entry_universes) env
+      in
+      let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in
+      let evd = Evd.from_env env'' in
+        (pth, Inductiveops.infer_inductive_subtyping env'' evd mind_ent)
+    end
+  else (pth, mind_ent)
+
+
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
 let inInductive : inductive_obj -> obj =
@@ -365,7 +380,8 @@ let inInductive : inductive_obj -> obj =
     open_function = open_inductive;
     classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
-    discharge_function = discharge_inductive }
+    discharge_function = discharge_inductive;
+    rebuild_function = infer_inductive_subtyping }
 
 let declare_projections mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
diff --git a/vernac/command.ml b/vernac/command.ml
index 35b75370e..2d4f05134 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -660,7 +660,10 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       mind_entry_private = if prv then Some false else None;
       mind_entry_universes = ground_uinfind;
     }
-  in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls
+  in
+  (if poly then
+      Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent
+   else mind_ent), pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 21ffa4cbf..c7a741c13 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -111,24 +111,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     | Some None -> Some None
     | None -> None
   in
-  let mind_ent =
-    { mind_entry_record = record;
-      mind_entry_finite = mib.mind_finite;
-      mind_entry_params = params';
-      mind_entry_inds = inds';
-      mind_entry_polymorphic = mib.mind_polymorphic;
-      mind_entry_private = mib.mind_private;
-      mind_entry_universes = univ_info_ind
-    }
-  in
-  if mib.mind_polymorphic then
-    begin
-      let env = Global.env () in
-      let env' = Environ.push_context univs env in
-      let (env'', typed_params) = Typeops.infer_local_decls env' params' in
-      let evd = Evd.from_env env'' in
-      Inductiveops.infer_inductive_subtyping env'' evd mind_ent
-    end
-  else
-    mind_ent
+  { mind_entry_record = record;
+    mind_entry_finite = mib.mind_finite;
+    mind_entry_params = params';
+    mind_entry_inds = inds';
+    mind_entry_polymorphic = mib.mind_polymorphic;
+    mind_entry_private = mib.mind_private;
+    mind_entry_universes = univ_info_ind
+  }