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.

23 files changed, 276 insertions, 125 deletions

diff --git a/API/API.ml b/API/API.ml
index 2b7bbd561..515b152e4 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -138,6 +138,7 @@ module Typeclasses = Typeclasses
 module Pretype_errors = Pretype_errors
 module Notation = Notation
 module Declarations = Declarations
+module Univops = Univops
 module Declareops = Declareops
 module Globnames = Globnames
 module Environ = Environ
diff --git a/API/API.mli b/API/API.mli
index cea879ba3..a4ae6347c 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1124,6 +1124,11 @@ sig
                             | SFBmodtype of module_type_body
 end
 
+module Univops : sig
+  val universes_of_constr : Term.constr -> Univ.LSet.t
+  val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
+end
+
 module Environ :
 sig
   type env = Prelude.env
@@ -2651,8 +2656,6 @@ sig
   val new_Type : Names.DirPath.t -> Term.types
   val unsafe_type_of_global : Globnames.global_reference -> Term.types
   val constr_of_global : Prelude.global_reference -> Term.constr
-  val universes_of_constr : Term.constr -> Univ.LSet.t
-  val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
   val new_univ_level : Names.DirPath.t -> Univ.Level.t
   val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context
   val new_sort_in_family : Sorts.family -> Sorts.t
diff --git a/dev/include b/dev/include
index 0f43f0072..4835b360d 100644
--- a/dev/include
+++ b/dev/include
@@ -41,6 +41,7 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* univ info *) ppuniverse_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6ae5125f6..e902da0b1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -215,6 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
+let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
diff --git a/engine/termops.ml b/engine/termops.ml
index 92016d4af..3eef71b2d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1173,6 +1173,9 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
       Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	f Reduction.CONV t1 t2 && f cv_pb c1 c2
+    | Const (c, u), Const (c', u') -> Constant.equal c c'
+    | Ind (i, _), Ind (i', _) -> eq_ind i i'
+    | Construct (i, _), Construct (i', _) -> eq_constructor i i'
     | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
 
 let constr_cmp sigma cv_pb t1 t2 =
diff --git a/engine/uState.ml b/engine/uState.ml
index acef90143..0973ca457 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -284,7 +284,7 @@ let universe_context ?names ctx =
         in map, ctx
 
 let restrict ctx vars =
-  let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in
+  let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
 type rigid = 
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 =
diff --git a/engine/universes.mli b/engine/universes.mli
index 1b9703c7b..c600f4af6 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -210,10 +210,6 @@ val unsafe_type_of_global : Globnames.global_reference -> types
 val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
   universe_opt_subst -> constr -> constr
 
-(** Shrink a universe context to a restricted set of variables *)
-
-val universes_of_constr : constr -> universe_set
-val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
 val simplify_universe_context : universe_context_set -> 
   universe_context_set * universe_level_subst
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cdea468ad..883896652 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 2f49982ce..8132d6685 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 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
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index f779f68be..60cd77f40 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 4a4cf1baa..5de45cf2b 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 f139a8b33..114193329 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 000000000..e9383c6d9
--- /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 000000000..5b499c75b
--- /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
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index ee75d2908..da21f64ab 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,8 +153,8 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na ctx c =
   let open Term in
-  let vars = Universes.universes_of_constr c in
-  let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
+  let vars = Univops.universes_of_constr c in
+  let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
   mkConst(declare_constant (Id.of_string na) 
 	    (DefinitionEntry (definition_entry ~opaque:true
 				~univs:(Univ.ContextSet.to_context ctx) c),
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 ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 971ad78e6..e374f7b3b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1313,8 +1313,8 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
-let report_anomaly _ =
-  let e = UserError (None, Pp.str "Conversion test raised an anomaly") in
+let report_anomaly e =
+  let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in
   let e = CErrors.push e in
   iraise e
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5ec34a638..f5664aed0 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -343,8 +343,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	    nf t
 	  else t
 	in
-        let used_univs_body = Universes.universes_of_constr body in
-        let used_univs_typ = Universes.universes_of_constr typ in
+        let used_univs_body = Univops.universes_of_constr body in
+        let used_univs_typ = Univops.universes_of_constr typ in
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
@@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
 	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = restrict_universe_context ctx used_univs in
+          let ctx_body = Univops.restrict_universe_context ctx used_univs in
           (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
@@ -362,7 +362,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
            * constraints in which we merge the ones for the body and the ones
            * for the typ *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = restrict_universe_context ctx used_univs in
+          let ctx = Univops.restrict_universe_context ctx used_univs in
           let univs = Univ.ContextSet.to_context ctx in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 466b1350d..8d8e19811 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -80,30 +80,30 @@ let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
     (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
-let ind_scheme_kind_from_type =
-  declare_individual_scheme_object "_ind_nodep"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp)
-
-let ind_scheme_kind_from_prop =
-  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp)
-
-let ind_dep_scheme_kind_from_type =
-  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
-  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp)
+let rec_scheme_kind_from_type =
+  declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
+  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
 
 let rec_scheme_kind_from_prop =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
   (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)
 
-let rec_scheme_kind_from_type =
-  declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
-  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)
-
 let rec_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
   (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)
 
+let ind_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind_nodep"
+  (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp)
+
+let ind_dep_scheme_kind_from_type =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
+  (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp)
+
+let ind_scheme_kind_from_prop =
+  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
+  (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp)
+
 (* Case analysis *)
 
 let build_case_analysis_scheme_in_type dep sort ind =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index aba61146c..007b70bc0 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -114,8 +114,8 @@ let instance_hook k info global imps ?hook cst =
 let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
   let evm = 
-    let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
-				 (Universes.universes_of_constr term) in
+    let levels = Univ.LSet.union (Univops.universes_of_constr termtype) 
+				 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context evm levels 
   in
   let pl, uctx = Evd.universe_context ?names:pl evm in
@@ -420,6 +420,8 @@ let context poly l =
         let _ = Command.declare_definition id decl entry [] [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
-      let () = uctx := Univ.ContextSet.empty in
 	status && nstatus
-  in List.fold_left fn true (List.rev ctx)
+  in 
+  if Lib.sections_are_opened () then
+    Declare.declare_universe_context poly !uctx;
+  List.fold_left fn true (List.rev ctx)
diff --git a/vernac/command.ml b/vernac/command.ml
index 2d4f05134..116a7aee1 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