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.

---
 toplevel/discharge.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'toplevel')

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