From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Tue, 28 Mar 2017 19:24:02 +0200
Subject: Extend definition of inductives to include subtyping info

---
 vernac/command.ml   | 2 +-
 vernac/discharge.ml | 9 ++++++++-
 vernac/record.ml    | 4 ++--
 vernac/record.mli   | 3 ++-
 4 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 998e7803e..5f95a42a3 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = uctx;
+    mind_entry_universes = (uctx, Univ.UContext.empty);
   },
     pl, impls
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 65ade7887..9c70eb97e 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -86,6 +86,13 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
 	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
     else Univ.Instance.empty, mib.mind_universes
   in
+  let substsbt, univssbt = 
+    if mib.mind_polymorphic then 
+      let inst = Univ.UContext.instance mib.mind_subtyping in
+      let cstrs = Univ.UContext.constraints mib.mind_subtyping in
+	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
+    else Univ.Instance.empty, Univ.UContext.empty
+  in
   let inds =
     Array.map_to_list
       (fun mip ->
@@ -116,5 +123,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univs;
+    mind_entry_universes = (univs, univssbt);
   }
diff --git a/vernac/record.ml b/vernac/record.ml
index 2400fa681..5c76bb4b2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite poly ctx idstruc
+	let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
diff --git a/vernac/record.mli b/vernac/record.mli
index 3fd651db9..a380b041a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,8 @@ val declare_projections :
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
-  bool (** polymorphic?*) -> Univ.universe_context ->
+  bool (** polymorphic?*) ->
+  (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
-- 
cgit v1.2.3