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, 67 insertions, 27 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 882ea61a9..eb8a0c85a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -454,48 +454,88 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
   let rigids env evd sk term sk' term' =
-    let fall_back () =
+    let check_strict () =
       let univs = EConstr.eq_constr_universes evd term term' in
+      match univs with
+      | Some univs ->
+        begin
+          let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+          try Success (Evd.add_constraints evd cstrs)
+          with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+        end
+      | None ->
+        UnifFailure (evd, NotSameHead)
+    in
+    let first_try_strict_check cond u u' try_subtyping_constraints =
+      if cond then
+        let univs = EConstr.eq_constr_universes evd term term' in
         match univs with
         | Some univs ->
           begin
             let cstrs = Universes.to_constraints (Evd.universes evd) univs in
             try Success (Evd.add_constraints evd cstrs)
-            with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+            with Univ.UniverseInconsistency p -> try_subtyping_constraints ()
           end
         | None ->
           UnifFailure (evd, NotSameHead)
+      else
+        UnifFailure (evd, NotSameHead)
     in
     let compare_heads evd = 
       match EConstr.kind evd term, EConstr.kind evd term' with
       | Const (c, u), Const (c', u') ->
-        fall_back ()
+        check_strict ()
       | Ind (ind, u), Ind (ind', u') ->
-         let nparamsaplied = Stack.args_size sk in
-         let nparamsaplied' = Stack.args_size sk' in
-         if Names.eq_ind ind ind' then
-         begin
-           let mind = Environ.lookup_mind (fst ind) env in
-           if mind.Declarations.mind_polymorphic then
-           begin
-             let num_param_arity =
-               Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt)
-             in
-             if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
-                fall_back ()
-             else
-             begin
-               let uinfind = mind.Declarations.mind_universes in
-               let evd' = check_leq_inductives evd uinfind u u' in
-               Success (check_leq_inductives evd' uinfind u' u)
-             end
-           end
-           else
-             fall_back ()
-         end
-         else UnifFailure (evd, NotSameHead)
+        let check_subtyping_constraints () =
+          let nparamsaplied = Stack.args_size sk in
+          let nparamsaplied' = Stack.args_size sk' in
+          begin
+            let mind = Environ.lookup_mind (fst ind) env in
+            if mind.Declarations.mind_polymorphic then
+              begin
+                let num_param_arity =
+                  Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt)
+                in
+                if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
+                  UnifFailure (evd, NotSameHead)
+                else
+                  begin
+                    let uinfind = mind.Declarations.mind_universes in
+                    let evd' = check_leq_inductives evd uinfind u u' in
+                    Success (check_leq_inductives evd' uinfind u' u)
+                  end
+              end
+            else
+              UnifFailure (evd, NotSameHead)
+          end
+        in
+        first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints
       | Construct (cons, u), Construct (cons', u') ->
-          fall_back ()
+        let check_subtyping_constraints () =
+          let ind, ind' = fst cons, fst cons' in
+          let j, j' = snd cons, snd cons' in
+          let nparamsaplied = Stack.args_size sk in
+          let nparamsaplied' = Stack.args_size sk' in
+          let mind = Environ.lookup_mind (fst ind) 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 ind).Declarations.mind_consnrealargs.(j - 1)
+              in
+              if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then
+                UnifFailure (evd, NotSameHead)
+              else
+                begin
+                  let uinfind = mind.Declarations.mind_universes in
+                  let evd' = check_leq_inductives evd uinfind u u' in
+                  Success (check_leq_inductives evd' uinfind u' u)
+                end
+            end
+          else
+            UnifFailure (evd, NotSameHead)
+        in
+        first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints
       | _, _ -> anomaly (Pp.str "")
     in
     ise_and evd [(fun i ->