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.

1 files changed, 5 insertions, 5 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 10b4915a2..92bace745 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)