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.

8 files changed, 162 insertions, 28 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cdea468adf..8838966520 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,6 +49,11 @@ let instantiate cb c =
     Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
   else c
 
+let instantiate_constraints cb cst =
+  if cb.const_polymorphic then 
+    Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst
+  else cst
+
 let body_of_constant otab cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (instantiate cb (force_constr c))
@@ -61,13 +66,15 @@ let type_of_constant cb =
       if t' == t then x else RegularArity t'
   | TemplateArity _ as x -> x
 
-let constraints_of_constant otab cb = Univ.Constraint.union 
-  (Univ.UContext.constraints cb.const_universes)
-  (match cb.const_body with
-  | Undef _ -> Univ.empty_constraint
-  | Def c -> Univ.empty_constraint
-  | OpaqueDef o ->
-      Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
+let constraints_of_constant otab cb =
+  let cst = Univ.Constraint.union 
+    (Univ.UContext.constraints cb.const_universes)
+    (match cb.const_body with
+    | Undef _ -> Univ.empty_constraint
+    | Def c -> Univ.empty_constraint
+    | OpaqueDef o ->
+        Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
+   in instantiate_constraints cb cst
 
 let universes_of_constant otab cb = 
   match cb.const_body with
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 2f49982ce2..8132d66850 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,3 +43,4 @@ Vm
 Csymtable
 Vconv
 Declarations
+Univops
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c8fad60ebe..a872a103a5 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
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f779f68be4..60cd77f402 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -90,6 +90,7 @@ let check_conv_error error why cst poly u f env a1 a2 =
 	else error (IncompatiblePolymorphism (env, a1, a2))
       else Constraint.union cst cst'
   with NotConvertible -> error why
+     | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
 
 (* for now we do not allow reorderings *)
 
@@ -302,6 +303,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	  let ctx2 = Univ.instantiate_univ_context cb2.const_universes in
 	  let inst1, ctx1 = Univ.UContext.dest ctx1 in
 	  let inst2, ctx2 = Univ.UContext.dest ctx2 in
+          output_string stderr "\ninst1:\n";
+          output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst1));
+          output_string stderr "\ninst2:\n";
+          output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst2)); flush stderr;
 	    if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
 	      error IncompatibleInstances
 	    else 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 4a4cf1baa7..5de45cf2b9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -725,8 +725,11 @@ struct
       pp_std ++ prl u1 ++ pr_constraint_type op ++
 	prl u2 ++ fnl () )  c (str "")
 
+  let universes_of c =
+    fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
 end
 
+let universes_of_constraints = Constraint.universes_of
 let empty_constraint = Constraint.empty
 let union_constraint = Constraint.union
 let eq_constraint = Constraint.equal
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f139a8b334..1141933293 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -462,3 +462,6 @@ val eq_levels : universe_level -> universe_level -> bool
 
 (** deprecated: Equality of formal universe expressions. *)
 val equal_universes : universe -> universe -> bool
+
+(** Universes of constraints *)
+val universes_of_constraints : constraints -> universe_set
diff --git a/kernel/univops.ml b/kernel/univops.ml
new file mode 100644
index 0000000000..e9383c6d9f
--- /dev/null
+++ b/kernel/univops.ml
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Univ
+open Declarations
+
+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 universes_of_inductive mind =
+  if mind.mind_polymorphic then
+  begin
+    let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in
+    let univ_of_one_ind oind = 
+      let arity_univs =
+        Context.Rel.fold_outside
+          (fun decl unvs ->
+             Univ.LSet.union
+              (Context.Rel.Declaration.fold_constr
+                 (fun cnstr unvs ->
+                    let cnstr = Vars.subst_instance_constr u cnstr in
+                    Univ.LSet.union
+                      (universes_of_constr cnstr) unvs)
+              decl Univ.LSet.empty) unvs)
+        oind.mind_arity_ctxt ~init:Univ.LSet.empty
+      in
+      Array.fold_left (fun unvs cns ->
+          let cns = Vars.subst_instance_constr u cns in
+          Univ.LSet.union (universes_of_constr cns) unvs) arity_univs 
+       oind.mind_nf_lc
+    in
+    let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in
+    let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in
+    let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in
+    univs
+  end
+  else LSet.empty
+
+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
diff --git a/kernel/univops.mli b/kernel/univops.mli
new file mode 100644
index 0000000000..5b499c75bc
--- /dev/null
+++ b/kernel/univops.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Univ
+open Declarations
+
+(** Shrink a universe context to a restricted set of variables *)
+
+val universes_of_constr : constr -> universe_set
+val universes_of_inductive : mutual_inductive_body -> universe_set
+val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set