From 9b3a234e4cf002292ca4a67e1b72daac463b4c46 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 21 Jun 2014 16:08:53 +0200
Subject: When discharging polymorphic definitions, we must take into account
 all polymorphic variables of the section as they might incur universe
 constraints that were used to typecheck the body of the definition, even if
 the variable itself was not used. For "Monomorphic" variables, their
 constraints are already always pushed to the global context. This fixes bug #
 3330.

---
 library/lib.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/library/lib.ml b/library/lib.ml
index 10b4915a29..92bace745c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -406,7 +406,9 @@ let extract_hyps (secs,ohyps) =
     | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
       let l, r = aux (idl,hyps) in 
 	(id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | (id::idl,hyps) -> aux (idl,hyps)
+    | ((_,_,poly,ctx)::idl,hyps) -> 
+        let l, r = aux (idl,hyps) in
+          l, if poly then Univ.ContextSet.union r ctx else r
     | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
@@ -430,13 +432,11 @@ let add_section_replacement f g hyps =
 
 let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-  add_section_replacement f f
+    add_section_replacement f f
 
 let add_section_constant is_projection kn =
-  (* let g x (l1,l2) = (Names.Cmap.add kn (Univ.Instance.empty,[||]) l1,l2) in *)
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    (* if is_projection then add_section_replacement g f *)
-    (* else *) add_section_replacement f f
+    add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
 
-- 
cgit v1.2.3