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, 6 insertions, 6 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index 2d4f051345..116a7aee16 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -106,7 +106,7 @@ let interp_definition pl bl p red_option c ctypopt =
 	let c = EConstr.Unsafe.to_constr c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-	let vars = Universes.universes_of_constr body in
+	let vars = Univops.universes_of_constr body in
 	let evd = Evd.restrict_universe_context !evdref vars in
 	let pl, uctx = Evd.universe_context ?names:pl evd in
  	imps1@(Impargs.lift_implicits nb_args imps2), pl,
@@ -131,8 +131,8 @@ let interp_definition pl bl p red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let vars = Univ.LSet.union (Universes.universes_of_constr body) 
-          (Universes.universes_of_constr typ) in
+        let vars = Univ.LSet.union (Univops.universes_of_constr body) 
+          (Univops.universes_of_constr typ) in
         let ctx = Evd.restrict_universe_context !evdref vars in
 	let pl, uctx = Evd.universe_context ?names:pl ctx in
 	imps1@(Impargs.lift_implicits nb_args impsty), pl,
@@ -329,7 +329,7 @@ let do_assumptions_bound_univs coe kind nl id pl c =
   let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
   let ty = EConstr.Unsafe.to_constr ty in
   let ty = nf ty in
-  let vars = Universes.universes_of_constr ty in
+  let vars = Univops.universes_of_constr ty in
   let evd = Evd.restrict_universe_context !evdref vars in
   let pl, uctx = Evd.universe_context ?names:pl evd in
   let uctx = Univ.ContextSet.of_context uctx in
@@ -1213,7 +1213,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+    let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
@@ -1245,7 +1245,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Universes.universes_of_constr (List.hd fixdecls) in
+    let vars = Univops.universes_of_constr (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in