Squashed commit of the following:

Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.

This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!

commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon Apr 24 17:14:21 2017 +0200

    Revert STL to monomorphic

commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon Apr 24 17:02:42 2017 +0200

    Try unifying universes before apply subtyping

commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany <amintimany@gmail.com>
Date:   Sun Apr 23 13:49:04 2017 +0200

    Compile more of STL with universe polymorphism

commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany <amintimany@gmail.com>
Date:   Tue Apr 18 21:26:45 2017 +0200

    Made more progress on compiling the standard library

commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany <amintimany@gmail.com>
Date:   Sun Apr 16 22:55:19 2017 +0200

    Make more number theoretic modules monomorphic

commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany <amintimany@gmail.com>
Date:   Fri Apr 14 16:11:48 2017 +0200

    WIP more of standard library compiles

    Also: Matthieu fixed a bug in rewrite system which was faulty when
    introducing new morphisms (Add Morphism) command.

commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany <amintimany@gmail.com>
Date:   Fri Apr 14 11:39:21 2017 +0200

    WIP: more of the standard library compiles

    We have implemented convertibility of constructors up-to mutual
    subtyping of their corresponding inductive types. This is similar to
    the behavior of template polymorphism.

commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany <amintimany@gmail.com>
Date:   Wed Apr 12 19:02:39 2017 +0200

    WIP: trying to get the standard library compile with universe polymorphism

    We are trying to prune universes after section ends. Sections add a
    load of universes that are not appearing in the body, type or the
    constraints.

1 files changed, 49 insertions, 21 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c8fad60eb..a872a103a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -489,8 +489,8 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if eq_ind ind1 ind2
-	then
+      if eq_ind ind1 ind2
+      then
         begin
           let fall_back () =
             let cuniv = convert_instances ~flex:false u1 u2 cuniv in
@@ -498,31 +498,54 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           in
           let mind = Environ.lookup_mind (fst ind1) env in
           if mind.Declarations.mind_polymorphic then
-          begin
-            let num_param_arity =
-              Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
-            in
-            if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
-              fall_back ()
-            else
             begin
-              let uinfind = mind.Declarations.mind_universes in
-              let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-              let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
-              convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+              let num_param_arity =
+                Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
+              in
+              if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
+                fall_back ()
+              else
+                begin
+                  let uinfind = mind.Declarations.mind_universes in
+                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+                  let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
+                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+                end
             end
-          end
           else
             fall_back ()
         end
-        else raise NotConvertible
+      else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	if Int.equal j1 j2 && eq_ind ind1 ind2
-	then
-	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-           convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv)
-        else raise NotConvertible
+      if Int.equal j1 j2 && eq_ind ind1 ind2
+      then
+        begin
+          let fall_back () =
+            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          in
+          let mind = Environ.lookup_mind (fst ind1) env in
+          if mind.Declarations.mind_polymorphic then
+            begin
+              let num_cnstr_args =
+                let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in
+                nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1)
+              in
+              if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then
+                fall_back ()
+              else
+                begin (* we don't consider subtyping for constructors. *)
+                  let uinfind = mind.Declarations.mind_universes in
+                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+                  let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in
+                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+                end
+            end
+          else
+            fall_back ()
+        end
+      else raise NotConvertible
 	  
     (* Eta expansion of records *)
     | (FConstruct ((ind1,j1),u1), _) ->
@@ -688,7 +711,12 @@ let infer_cmp_universes env pb s0 s1 univs =
         else univs
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
-  (univs, Univ.enforce_eq_instances u u' cstrs)
+  let cstrs' =
+    if flex then 
+      if UGraph.check_eq_instances univs u u' then cstrs
+      else raise NotConvertible
+    else Univ.enforce_eq_instances u u' cstrs
+  in (univs, cstrs')
 
 let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in