From ead5d80dff08f97998e81acfb2562dde741a26af Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 3 Aug 2014 23:19:56 +0200
Subject: Fix infer conv using the wrong universe conversion flexibility
 information for constants that are not unfolded during conversion. Fix
 discharge of polymorphic section variables over inductive types.

---
 kernel/reduction.ml   | 5 +++--
 toplevel/discharge.ml | 1 +
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 28fe7141ff..78d2105ab0 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -199,8 +199,9 @@ let conv_table_key infos k1 k2 cuniv =
   | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' ->
     if Univ.Instance.equal u u' then cuniv
     else 
-      let flex = evaluable_constant cst (info_env infos) in
-	convert_instances flex u u' cuniv
+      let flex = evaluable_constant cst (info_env infos) 
+	&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
+      in convert_instances flex u u' cuniv
   | VarKey id, VarKey id' when Id.equal id id' -> cuniv
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 971ae70d86..9de0edea81 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -101,6 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
       mib.mind_packets in
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
+  let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
   let record = match mib.mind_record with
     | None -> None
-- 
cgit v1.2.3