From 012f5fb722a9d5dcef82c800aa54ed50c0a58957 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 19:11:20 +0200
Subject: Safe API for accessing universe constraints of global references.

Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
---
 vernac/obligations.ml | 2 +-
 vernac/record.ml      | 4 ++--
 vernac/search.ml      | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57d..5a1c260b1f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -362,7 +362,7 @@ let get_body obl =
   match obl.obl_body with
   | None -> None
   | Some (DefinedObl c) ->
-    let u = Environ.constant_instance (Global.env ()) c in
+    let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
     let pc = (c, u) in
       Some (DefinedObl pc)
   | Some (TermObl c) ->
diff --git a/vernac/record.ml b/vernac/record.ml
index d61f44cac8..366f504545 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,7 +265,7 @@ let warn_non_primitive_record =
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let u = Declareops.inductive_polymorphic_instance mib in
+  let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let poly = Declareops.inductive_is_polymorphic mib in
   let ctx =
@@ -547,7 +547,7 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
-    let inst = Declareops.inductive_polymorphic_instance mind in
+    let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
diff --git a/vernac/search.ml b/vernac/search.ml
index 00536e52ec..788a2aa4a9 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Declareops.inductive_polymorphic_instance mib in
+      let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in
-- 
cgit v1.2.3


From 40ec7bc85b78f68257593234016f82d8e78d6384 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Jul 2017 00:59:53 +0200
Subject: Properly handling polymorphic inductive subtyping in the kernel.

Before this patch, inductive subtyping was enforcing syntactic equality
of the variable instance, instead of reasoning up to alpha-renaming.
---
 vernac/himsg.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ca3fb392fe..86dcb6d4dc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,6 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
+      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
-- 
cgit v1.2.3