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, 0 insertions, 30 deletions

diff --git a/engine/universes.ml b/engine/universes.ml
index 51957e00a..a12b42ab1 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -976,36 +976,6 @@ let normalize_context_set ctx us algs =
 (* let normalize_conkey = Profile.declare_profile "normalize_context_set" *)
 (* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *)
 
-let universes_of_constr c =
-  let rec aux s c = 
-    match kind_of_term c with
-    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.fold LSet.add (Instance.levels u) s
-    | Sort u when not (Sorts.is_small u) -> 
-      let u = univ_of_sort u in
-      LSet.fold LSet.add (Universe.levels u) s
-    | _ -> fold_constr aux s c
-  in aux LSet.empty c
-
-let restrict_universe_context (univs,csts) s =
-  (* Universes that are not necessary to typecheck the term.
-     E.g. univs introduced by tactics and not used in the proof term. *)
-  let diff = LSet.diff univs s in
-  let rec aux diff candid univs ness = 
-    let (diff', candid', univs', ness') = 
-      Constraint.fold
-	(fun (l, d, r as c) (diff, candid, univs, csts) ->
-	  if not (LSet.mem l diff) then
-	    (LSet.remove r diff, candid, univs, Constraint.add c csts)
-	  else if not (LSet.mem r diff) then
-	    (LSet.remove l diff, candid, univs, Constraint.add c csts)
-	  else (diff, Constraint.add c candid, univs, csts))
-	candid (diff, Constraint.empty, univs, ness)
-    in
-      if ness' == ness then (LSet.diff univs diff', ness)
-      else aux diff' candid' univs' ness'
-  in aux diff csts univs Constraint.empty
-
 let simplify_universe_context (univs,csts) =
   let uf = UF.create () in
   let noneqs =