21 files changed, 374 insertions, 328 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 23d066df58..150dad16c2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -76,6 +76,7 @@ let mkProj (p, c) = of_kind (Proj (p, c))
 let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
 let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
 let mkInt i = of_kind (Int i)
+let mkFloat f = of_kind (Float f)
 
 let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstRef c -> mkConstU (c,u)
@@ -334,7 +335,7 @@ let iter_with_full_binders sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> ()
+    | Construct _ | Int _ | Float _) -> ()
   | Cast (c,_,t) -> f n c; f n t
   | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
   | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
@@ -462,16 +463,16 @@ let test_constr_universes env sigma leq m n =
       if Sorts.equal s1 s2 then true
       else (cstrs := Set.add
               (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
-	    true)
+            true)
     in
-    let leq_sorts s1 s2 = 
+    let leq_sorts s1 s2 =
       let s1 = ESorts.kind sigma s1 in
       let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
-      else 
+      else
         (cstrs := Set.add
            (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
-	 true)
+         true)
     in
     let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in
     let res =
@@ -495,20 +496,20 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   let kind c = kind sigma c in
   match kind m, kind n with
   | Proj (p, c), App (f, args)
-  | App (f, args), Proj (p, c) -> 
+  | App (f, args), Proj (p, c) ->
       (match kind f with
-      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
+      | Const (p', u) when Constant.equal (Projection.constant p) p' ->
           let npars = Projection.npars p in
           if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
-	  else false
+          else false
       | _ -> false)
   | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n
 
 let eq_constr_universes_proj env sigma m n =
   let open UnivProblem in
   if m == n then Some Set.empty
-  else 
+  else
     let cstrs = ref Set.empty in
     let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in
     let eq_sorts s1 s2 =
@@ -518,7 +519,7 @@ let eq_constr_universes_proj env sigma m n =
       else
         (cstrs := Set.add
            (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
-	 true)
+         true)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' nargs m n
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2afce38db7..90f50b764c 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -127,6 +127,7 @@ val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
 val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
+val mkFloat : Float64.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ea71be8e43..b09cc87f97 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -562,19 +562,19 @@ let rec check_and_clear_in_constr env evdref err ids global c =
         c
 
       | Evar (evk,l as ev) ->
-	  if Evd.is_defined !evdref evk then
-	    (* If evk is already defined we replace it by its definition *)
+          if Evd.is_defined !evdref evk then
+            (* If evk is already defined we replace it by its definition *)
             let nc = Evd.existential_value !evdref (EConstr.of_existential ev) in
             let nc = EConstr.Unsafe.to_constr nc in
-	      (check_and_clear_in_constr env evdref err ids global nc)
-	  else
-	    (* We check for dependencies to elements of ids in the
-	       evar_info corresponding to e and in the instance of
-	       arguments. Concurrently, we build a new evar
-	       corresponding to e where hypotheses of ids have been
-	       removed *)
-	    let evi = Evd.find_undefined !evdref evk in
-	    let ctxt = Evd.evar_filtered_context evi in
+              (check_and_clear_in_constr env evdref err ids global nc)
+          else
+            (* We check for dependencies to elements of ids in the
+               evar_info corresponding to e and in the instance of
+               arguments. Concurrently, we build a new evar
+               corresponding to e where hypotheses of ids have been
+               removed *)
+            let evi = Evd.find_undefined !evdref evk in
+            let ctxt = Evd.evar_filtered_context evi in
             let (rids,filter) =
               List.fold_right2
                 (fun h a (ri,filter) ->
@@ -594,11 +594,11 @@ let rec check_and_clear_in_constr env evdref err ids global c =
                   (* No dependency at all, we can keep this ev's context hyp *)
                     (ri, true::filter)
                   with Depends id -> (Id.Map.add (NamedDecl.get_id h) id ri, false::filter))
-		ctxt (Array.to_list l) (Id.Map.empty,[]) in
-	    (* Check if some rid to clear in the context of ev has dependencies
-	       in the type of ev and adjust the source of the dependency *)
-	    let _nconcl =
-	      try
+                ctxt (Array.to_list l) (Id.Map.empty,[]) in
+            (* Check if some rid to clear in the context of ev has dependencies
+               in the type of ev and adjust the source of the dependency *)
+            let _nconcl =
+              try
                 let nids = Id.Map.domain rids in
                 let global = Id.Set.exists is_section_variable nids in
                 let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
@@ -661,26 +661,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
 (* spiwack: a few functions to gather evars on which goals depend. *)
 let queue_set q is_dependent set =
   Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term evm q is_dependent c =
-  queue_set q is_dependent (evars_of_term evm c)
+let queue_term q is_dependent c =
+  queue_set q is_dependent (evar_nodes_of_term c)
 
 let process_dependent_evar q acc evm is_dependent e =
   let evi = Evd.find evm e in
   (* Queues evars appearing in the types of the goal (conclusion, then
      hypotheses), they are all dependent. *)
-  queue_term evm q true evi.evar_concl;
+  queue_term q true evi.evar_concl;
   List.iter begin fun decl ->
     let open NamedDecl in
-    queue_term evm q true (NamedDecl.get_type decl);
+    queue_term q true (NamedDecl.get_type decl);
     match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> queue_term evm q true b
+    | LocalDef (_,b,_) -> queue_term q true b
   end (EConstr.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
       if is_dependent then Evar.Map.add e None acc else acc
   | Evar_defined b ->
-      let subevars = evars_of_term evm b in
+      let subevars = evar_nodes_of_term b in
       (* evars appearing in the definition of an evar [e] are marked
          as dependent when [e] is dependent itself: if [e] is a
          non-dependent goal, then, unless they are reach from another
@@ -694,7 +694,7 @@ let gather_dependent_evars q evm =
     let (is_dependent,e) = Queue.pop q in
     (* checks if [e] has already been added to [!acc] *)
     begin if not (Evar.Map.mem e !acc) then
-        acc := process_dependent_evar q !acc evm is_dependent e  
+        acc := process_dependent_evar q !acc evm is_dependent e
     end
   done;
   !acc
@@ -736,7 +736,7 @@ let undefined_evars_of_term evd t =
     match EConstr.kind evd c with
       | Evar (n, l) ->
         let acc = Evar.Set.add n acc in
-	Array.fold_left evrec acc l
+        Array.fold_left evrec acc l
       | _ -> EConstr.fold evd evrec acc c
   in
   evrec Evar.Set.empty t
@@ -751,10 +751,10 @@ let undefined_evars_of_evar_info evd evi =
   Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
     (Evar.Set.union
        (match evi.evar_body with
-	 | Evar_empty -> Evar.Set.empty
+         | Evar_empty -> Evar.Set.empty
          | Evar_defined b -> undefined_evars_of_term evd b)
        (undefined_evars_of_named_context evd
-	  (named_context_of_val evi.evar_hyps)))
+          (named_context_of_val evi.evar_hyps)))
 
 type undefined_evars_cache = {
   mutable cache : (EConstr.named_declaration * Evar.Set.t) ref Id.Map.t;
@@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' =
   in
   Evd.add_universe_constraints evd soft
 
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extension of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+    [t] and [u] up to existential variable instantiation and
+    equalisable universes. The term [t] is interpreted in [evd] while
+    [u] is interpreted in [extended_evd]. The universe constraints in
+    [extended_evd] are assumed to be an extension of those in [evd]. *)
+let eq_constr_univs_test ~evd ~extended_evd t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
   let t = EConstr.Unsafe.to_constr t
@@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u =
   in
   let ans =
     UnivProblem.eq_constr_univs_infer_with
-      (fun t -> kind_of_term_upto sigma1 t)
-      (fun u -> kind_of_term_upto sigma2 u)
-      (universes sigma2) fold t u sigma2
+      (fun t -> kind_of_term_upto evd t)
+      (fun u -> kind_of_term_upto extended_evd u)
+      (universes extended_evd) fold t u extended_evd
   in
   match ans with None -> false | Some _ -> true
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index e9d579af32..65a069a280 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -58,7 +58,7 @@ val new_pure_evar :
 
 val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 
-(** Create a new Type existential variable, as we keep track of 
+(** Create a new Type existential variable, as we keep track of
     them during type-checking and unification. *)
 val new_type_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
@@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
 val kind_of_term_upto : evar_map -> Constr.constr ->
   (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term
 
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extension of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+    [t] and [u] up to existential variable instantiation and
+    equalisable universes. The term [t] is interpreted in [evd] while
+    [u] is interpreted in [extended_evd]. The universe constraints in
+    [extended_evd] are assumed to be an extension of those in [evd]. *)
+val eq_constr_univs_test :
+    evd:Evd.evar_map ->
+    extended_evd:Evd.evar_map ->
+    constr ->
+    constr ->
+    bool
 
 (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
    [Inl sigma'] where [sigma'] is [sigma] augmented with universe
diff --git a/engine/evd.ml b/engine/evd.ml
index b621a3fe2f..94868d9bdd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -652,7 +652,7 @@ let existential_type0 = existential_type
 let add_constraints d c =
   { d with universes = UState.add_constraints d.universes c }
 
-let add_universe_constraints d c = 
+let add_universe_constraints d c =
   { d with universes = UState.add_universe_constraints d.universes c }
 
 (*** /Lifting... ***)
@@ -664,7 +664,7 @@ let is_empty d =
   List.is_empty d.conv_pbs &&
   Metamap.is_empty d.metas
 
-let cmap f evd = 
+let cmap f evd =
   { evd with
       metas = Metamap.map (map_clb f) evd.metas;
       defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
@@ -701,8 +701,8 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env e = 
-  { empty with universes = UState.make (Environ.universes e) }
+let from_env e =
+  { empty with universes = UState.make ~lbound:(Environ.universes_lbound e) (Environ.universes e) }
 
 let from_ctx ctx = { empty with universes = ctx }
 
@@ -711,7 +711,7 @@ let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
-  let universes = 
+  let universes =
     if not with_univs then evd.universes
     else UState.union evd.universes d.universes
   in
@@ -812,10 +812,10 @@ let extract_conv_pbs evd p =
   let (pbs,pbs1) =
     List.fold_left
       (fun (pbs,pbs1) pb ->
-    	 if p pb then
-	   (pb::pbs,pbs1)
+         if p pb then
+           (pb::pbs,pbs1)
          else
-	   (pbs,pb::pbs1))
+           (pbs,pb::pbs1))
       ([],[])
       evd.conv_pbs
   in
@@ -864,9 +864,9 @@ let universe_subst evd =
   UState.subst evd.universes
 
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
-  {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff rigid evd.universes ctx'}
 
-let merge_universe_subst evd subst = 
+let merge_universe_subst evd subst =
   {evd with universes = UState.merge_subst evd.universes subst }
 
 let with_context_set ?loc rigid d (a, ctx) =
@@ -915,7 +915,7 @@ let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
 
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
-let is_flexible_level evd l = 
+let is_flexible_level evd l =
   let uctx = evd.universes in
     Univ.LMap.mem l (UState.subst uctx)
 
@@ -947,7 +947,7 @@ let normalize_universe_instance evd l =
 let normalize_sort evars s =
   match s with
   | SProp | Prop | Set -> s
-  | Type u -> 
+  | Type u ->
     let u' = normalize_universe evars u in
     if u' == u then s else Sorts.sort_of_univ u'
 
@@ -974,7 +974,7 @@ let set_eq_instances ?(flex=false) d u1 u2 =
     (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty)
 
 let set_leq_sort env evd s1 s2 =
-  let s1 = normalize_sort evd s1 
+  let s1 = normalize_sort evd s1
   and s2 = normalize_sort evd s2 in
   match is_eq_sort s1 s2 with
   | None -> evd
@@ -982,7 +982,7 @@ let set_leq_sort env evd s1 s2 =
      if not (type_in_type env) then
        add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2)))
      else evd
-	    
+
 let check_eq evd s s' =
   UGraph.check_eq (UState.ugraph evd.universes) s s'
 
@@ -1256,7 +1256,7 @@ type 'a sigma = {
 
 let sig_it x = x.it
 let sig_sig x = x.sigma
-let on_sig s f = 
+let on_sig s f =
   let sigma', v = f s.sigma in
     { s with sigma = sigma' }, v
 
@@ -1403,7 +1403,16 @@ end
 
 let evars_of_term evd c =
   let rec evrec acc c =
-    match MiniEConstr.kind evd c with
+    let c = MiniEConstr.whd_evar evd c in
+    match kind c with
+    | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+    | _ -> Constr.fold evrec acc c
+  in
+  evrec Evar.Set.empty c
+
+let evar_nodes_of_term c =
+  let rec evrec acc c =
+    match kind c with
     | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
     | _ -> Constr.fold evrec acc c
   in
diff --git a/engine/evd.mli b/engine/evd.mli
index 132f7bc745..7876e9a48f 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -141,7 +141,7 @@ val empty : evar_map
 (** The empty evar map. *)
 
 val from_env : env -> evar_map
-(** The empty evar map with given universe context, taking its initial 
+(** The empty evar map with given universe context, taking its initial
     universes from env. *)
 
 val from_ctx : UState.t -> evar_map
@@ -251,7 +251,7 @@ val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info
 
 val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr
 
-val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> 
+val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
   evar_map ->  evar_map -> evar_map
 (** spiwack: this function seems to somewhat break the abstraction. *)
 
@@ -509,6 +509,10 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 val evars_of_term : evar_map -> econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
+val evar_nodes_of_term : econstr -> Evar.Set.t
+  (** same as evars_of_term but also including defined evars.
+      For use in printing dependent evars *)
+
 val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
@@ -592,8 +596,8 @@ val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_
 val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
 (** See [UState.make_nonalgebraic_variable]. *)
 
-val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option 
-(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
+val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
+(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
     not a local sort variable declared in [evm] *)
 
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
@@ -606,7 +610,7 @@ val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
 val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
 val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
-val set_eq_instances : ?flex:bool -> 
+val set_eq_instances : ?flex:bool ->
   evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
 
 val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 7c06bb59f1..3c383b2e00 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -30,7 +30,7 @@
 exception Exception of exn
 
 (** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
 
 (** This exception is used by the tactics to signal failure by lack of
     successes, rather than some other exceptions (like system
@@ -38,7 +38,6 @@ exception Timeout
 exception TacticFailure of exn
 
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!")
   | Exception e -> CErrors.print e
   | TacticFailure e -> CErrors.print e
   | _ -> raise CErrors.Unhandled
@@ -99,7 +98,7 @@ struct
   let print_char = fun c -> (); fun () -> print_char c
 
   let timeout = fun n t -> (); fun () ->
-    Control.timeout n t () (Exception Timeout)
+    Control.timeout n t () (Exception Tac_Timeout)
 
   let make f = (); fun () ->
     try f ()
@@ -108,7 +107,7 @@ struct
       Util.iraise (Exception e, info)
 
   (** Use the current logger. The buffer is also flushed. *)
-  let print_debug   s = make (fun _ -> Feedback.msg_info s)
+  let print_debug   s = make (fun _ -> Feedback.msg_debug s)
   let print_info    s = make (fun _ -> Feedback.msg_info s)
   let print_warning s = make (fun _ -> Feedback.msg_warning s)
   let print_notice  s = make (fun _ -> Feedback.msg_notice s)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 90c920439a..75920455ce 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -30,7 +30,7 @@
 exception Exception of exn
 
 (** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
 
 (** This exception is used by the tactics to signal failure by lack of
     successes, rather than some other exceptions (like system
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 89c2fade62..56277e8092 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
   in
   hdrec c
 
@@ -153,18 +153,19 @@ let hdchar env sigma c =
     | Var id  -> lowercase_first_char id
     | Sort s -> sort_hdchar (ESorts.kind sigma s)
     | Rel n ->
-	(if n<=k then "p" (* the initial term is flexible product/function *)
-	 else
+        (if n<=k then "p" (* the initial term is flexible product/function *)
+         else
            try match let d = lookup_rel (n-k) env in get_name d, get_type d with
              | Name id, _ -> lowercase_first_char id
              | Anonymous, t -> hdrec 0 (lift (n-k) t)
-	   with Not_found -> "y")
+           with Not_found -> "y")
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
-	lowercase_first_char id
+        lowercase_first_char id
     | Evar _ (* We could do better... *)
     | Meta _ | Case (_, _, _, _) -> "y"
     | Int _ -> "i"
+    | Float _ -> "f"
   in
   hdrec 0 c
 
@@ -195,7 +196,7 @@ let name_context env sigma hyps =
   snd
     (List.fold_left
        (fun (env,hyps) d ->
-	  let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
+          let d' = name_assumption env sigma d in (push_rel d' env, d' :: hyps))
        (env,[]) (List.rev hyps))
 
 let mkProd_or_LetIn_name env sigma b d = mkProd_or_LetIn (name_assumption env sigma d) b
@@ -355,8 +356,8 @@ let next_name_away_with_default_using_types default na avoid t =
   let id = match na with
     | Name id -> id
     | Anonymous -> match !reserved_type_name t with
-	| Name id -> id
-	| Anonymous -> Id.of_string default in
+        | Name id -> id
+        | Anonymous -> Id.of_string default in
   next_ident_away id avoid
 
 let next_name_away = next_name_away_with_default default_non_dependent_string
@@ -457,12 +458,12 @@ let rename_bound_vars_as_displayed sigma avoid env c =
   let rec rename avoid env c =
     match EConstr.kind sigma c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' =
+        let na',avoid' =
           compute_displayed_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
         mkProd ({na with binder_name=na'}, c1, rename avoid' (na' :: env) c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' =
+        let na',avoid' =
           compute_displayed_let_name_in sigma
             (RenamingElsewhereFor (env,c2)) avoid na.binder_name c2 in
         mkLetIn ({na with binder_name=na'},c1,t, rename avoid' (na' :: env) c2)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 7a8544f2d6..4a1cd4d44f 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -88,7 +88,7 @@ val next_ident_away : Id.t -> Id.Set.t -> Id.t
 (** Avoid clashing with a name already used in current module *)
 val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t
 
-(** Avoid clashing with a name already used in current module 
+(** Avoid clashing with a name already used in current module
    but tolerate overwriting section variables, as in goals *)
 val next_global_ident_away : Id.t -> Id.Set.t -> Id.t
 
diff --git a/engine/nameops.ml b/engine/nameops.ml
index baa19050d7..fe0a91e3ba 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -72,13 +72,13 @@ let cut_ident skip_quote s =
     else
       let c = Char.code (String.get s (n-1)) in
       if Int.equal c code_of_0 && not (Int.equal n slen) then
-	numpart (n-1) n'
+        numpart (n-1) n'
       else if code_of_0 <= c && c <= code_of_9 then
-	numpart (n-1) (n-1)
+        numpart (n-1) (n-1)
       else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then
-	numpart (n-1) (n-1)
+        numpart (n-1) (n-1)
       else
-	n'
+        n'
   in
   numpart slen slen
 
@@ -126,20 +126,20 @@ let increment_subscript id =
     let c = id.[carrypos] in
     if is_digit c then
       if Int.equal (Char.code c) (Char.code '9') then begin
-	assert (carrypos>0);
-	add (carrypos-1)
+        assert (carrypos>0);
+        add (carrypos-1)
       end
       else begin
-	let newid = Bytes.of_string id in
-	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
-	Bytes.set newid carrypos (Char.chr (Char.code c + 1));
-	newid
+        let newid = Bytes.of_string id in
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.set newid carrypos (Char.chr (Char.code c + 1));
+        newid
       end
     else begin
       let newid = Bytes.of_string (id^"0") in
       if carrypos < len-1 then begin
-	Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
-	Bytes.set newid (carrypos+1) '1'
+        Bytes.fill newid (carrypos+1) (len-1-carrypos) '0';
+        Bytes.set newid (carrypos+1) '1'
       end;
       newid
     end
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8b5bd4cd80..ed44372045 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -130,7 +130,7 @@ let focus_context (left,right) =
     i]. *)
 let focus_sublist i j l =
   let (left,sub_right) = CList.goto (i-1) l in
-  let (sub, right) = 
+  let (sub, right) =
     try CList.chop (j-i+1) sub_right
     with Failure _ -> raise CList.IndexOutOfRange
   in
@@ -479,7 +479,7 @@ let fold_left2_goal i s l =
   let err =
     return () >>= fun () -> (* Delay the computation of list lengths. *)
     tclZERO (SizeMismatch (CList.length initial.comb,CList.length l))
-  in 
+  in
   Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
     Solution.get >>= fun step ->
     match cleared_alias step goal with
@@ -515,7 +515,7 @@ let fold_left2_goal i s l =
 let tclDISPATCHGEN0 join tacs =
   match tacs with
   | [] ->
-      begin 
+      begin
         let open Proof in
         Comb.get >>= function
         | [] -> tclUNIT (join [])
@@ -849,7 +849,8 @@ let give_up =
 
 module Progress = struct
 
-  let eq_constr = Evarutil.eq_constr_univs_test
+  let eq_constr evd extended_evd =
+    Evarutil.eq_constr_univs_test ~evd ~extended_evd
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
@@ -879,10 +880,10 @@ module Progress = struct
     eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
 
   (** Equality function on goals *)
-  let goal_equal evars1 gl1 evars2 gl2 =
-    let evi1 = Evd.find evars1 gl1 in
-    let evi2 = Evd.find evars2 gl2 in
-    eq_evar_info evars1 evars2 evi1 evi2
+  let goal_equal ~evd ~extended_evd evar extended_evar =
+    let evi = Evd.find evd evar in
+    let extended_evi = Evd.find extended_evd extended_evar in
+    eq_evar_info evd extended_evd evi extended_evi
 
 end
 
@@ -899,17 +900,17 @@ let tclPROGRESS t =
   let test =
     quick_test ||
     Util.List.for_all2eq begin fun i f ->
-      Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
+      Progress.goal_equal ~evd:initial.solution
+        ~extended_evd:final.solution (drop_state i) (drop_state f)
     end initial.comb final.comb
   in
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
 
-exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -934,7 +935,8 @@ let tclTIMEOUT n t =
       end
       begin let open Logic_monad.NonLogical in function (e, info) ->
         match e with
-        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+        | Logic_monad.Tac_Timeout ->
+          return (Util.Inr (Logic_monad.Tac_Timeout, info))
         | Logic_monad.TacticFailure e ->
           return (Util.Inr (e, info))
         | e -> Logic_monad.NonLogical.raise ~info e
@@ -1010,7 +1012,7 @@ module Unsafe = struct
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
-  let tclEVARUNIVCONTEXT ctx = 
+  let tclEVARUNIVCONTEXT ctx =
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
 
   let reset_future_goals p =
@@ -1227,7 +1229,7 @@ module V82 = struct
     let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in
     { ps with solution = evd; }
     end
-      
+
   let has_unresolved_evar pv =
     Evd.has_undefined pv.solution
 
@@ -1236,8 +1238,8 @@ module V82 = struct
     let undef = Evd.undefined_map pv.solution in
     let goals = CList.rev_map fst (Evar.Map.bindings undef) in
     { pv with comb = List.map with_empty_state goals }
-      
-    
+
+
 
   let top_goals initial { solution=solution; } =
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
@@ -1245,7 +1247,7 @@ module V82 = struct
 
   let top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term sigma c)
+      Evar.Set.elements (Evd.evar_nodes_of_term c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index f90f02f3e1..8ec53ac78c 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -145,7 +145,7 @@ val unfocus : focus_context -> proofview -> proofview
 
 
 (** The abstract type of tactics *)
-type +'a tactic 
+type +'a tactic
 
 (** Applies a tactic to the current proofview. Returns a tuple
     [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv]
@@ -170,7 +170,7 @@ val apply
 
 (** Unit of the tactic monad. *)
 val tclUNIT : 'a -> 'a tactic
- 
+
 (** Bind operation of the tactic monad. *)
 val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
 
@@ -398,14 +398,23 @@ val give_up : unit tactic
 val tclPROGRESS : 'a tactic -> 'a tactic
 
 module Progress : sig
-  val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool
+(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether
+    the [evar_info] from [evd] corresponding to [evar] is equal to that
+    from [extended_evd] corresponding to [extended_evar], up to
+    existential variable instantiation and equalisable universes. The
+    universe constraints in [extended_evd] are assumed to be an
+    extension of the universe constraints in [evd]. *)
+  val goal_equal :
+    evd:Evd.evar_map ->
+    extended_evd:Evd.evar_map ->
+    Evar.t ->
+    Evar.t ->
+    bool
 end
 
 (** Checks for interrupts *)
 val tclCHECKINTERRUPT : unit tactic
 
-exception Timeout
-
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
@@ -431,7 +440,7 @@ module Unsafe : sig
       goal. If goals have been solved in [sigma] they will still
       appear as unsolved goals. *)
   val tclEVARS : Evd.evar_map -> unit tactic
-    
+
   (** Like {!tclEVARS} but also checks whether goals have been solved. *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 2ab2f60421..a65b8275e6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -95,15 +95,15 @@ let pr_meta_map env sigma =
     | _ -> mt() in
   let pr_meta_binding = function
     | (mv,Cltyp (na,b)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " : " ++
+        hov 0
+          (pr_meta mv ++ pr_name na ++ str " : " ++
            print_constr env sigma b.rebus ++ fnl ())
     | (mv,Clval(na,(b,s),t)) ->
-      	hov 0
-	  (pr_meta mv ++ pr_name na ++ str " := " ++
+        hov 0
+          (pr_meta mv ++ pr_name na ++ str " := " ++
            print_constr env sigma b.rebus ++
            str " : " ++ print_constr env sigma t.rebus ++
-	   spc () ++ pr_instance_status s ++ fnl ())
+           spc () ++ pr_instance_status s ++ fnl ())
   in
   prlist pr_meta_binding (meta_list sigma)
 
@@ -232,7 +232,7 @@ let pr_evar_universe_context ctx =
   let prl = pr_uctx_level ctx in
   if UState.is_empty ctx then mt ()
   else
-    (str"UNIVERSES:"++brk(0,1)++ 
+    (str"UNIVERSES:"++brk(0,1)++
        h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
@@ -387,10 +387,10 @@ let pr_var_decl env decl =
   let pbody = match decl with
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
-	(* Force evaluation *)
-	let c = EConstr.of_constr c in
+        (* Force evaluation *)
+        let c = EConstr.of_constr c in
         let pb = print_constr_env env sigma c in
-	  (str" := " ++ pb ++ cut () ) in
+          (str" := " ++ pb ++ cut () ) in
   let pt = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
@@ -401,10 +401,10 @@ let pr_rel_decl env decl =
   let pbody = match decl with
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
-	(* Force evaluation *)
-	let c = EConstr.of_constr c in
+        (* Force evaluation *)
+        let c = EConstr.of_constr c in
         let pb = print_constr_env env sigma c in
-	  (str":=" ++ spc () ++ pb ++ spc ()) in
+          (str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = print_constr_env env sigma (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -412,13 +412,13 @@ let pr_rel_decl env decl =
 
 let print_named_context env =
   hv 0 (fold_named_context
-	  (fun env d pps ->
-	    pps ++ ws 2 ++ pr_var_decl env d)
+          (fun env d pps ->
+            pps ++ ws 2 ++ pr_var_decl env d)
           env ~init:(mt ()))
 
 let print_rel_context env =
   hv 0 (fold_rel_context
-	  (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
+          (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
           env ~init:(mt ()))
 
 let print_env env =
@@ -426,7 +426,7 @@ let print_env env =
     fold_named_context
       (fun env d pps ->
          let pidt =  pr_var_decl env d in
-	 (pps ++ fnl () ++ pidt))
+         (pps ++ fnl () ++ pidt))
       env ~init:(mt ())
   in
   let db_env =
@@ -517,9 +517,9 @@ let it_mkLambda_or_LetIn_from_no_LetIn c decls =
 let rec strip_head_cast sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 = match EConstr.kind sigma f with
-	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| Cast (c,_,_) -> collapse_rec c cl2
-	| _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2)
+        | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+        | Cast (c,_,_) -> collapse_rec c cl2
+        | _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2)
       in
       collapse_rec f cl
   | Cast (c,_,_) -> strip_head_cast sigma c
@@ -531,7 +531,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
   | App (f,args) when EConstr.isEvar sigma (Array.last args) ->
       let open EConstr in
       drop_extra_implicit_args sigma
-	(mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+        (mkApp (f,fst (Array.chop (Array.length args - 1) args)))
   | _ -> c
 
 (* Get the last arg of an application *)
@@ -600,28 +600,28 @@ let map_constr_with_binders_left_to_right sigma g f l c =
   let open EConstr in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> c
-  | Cast (b,k,t) -> 
-    let b' = f l b in 
+    | Construct _ | Int _ | Float _) -> c
+  | Cast (b,k,t) ->
+    let b' = f l b in
     let t' = f l t in
       if b' == b && t' == t then c
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
       let b' = f (g (LocalAssum (na,t)) l) b in
-	if t' == t && b' == b then c
-	else mkProd (na, t', b')
+        if t' == t && b' == b then c
+        else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
       let b' = f (g (LocalAssum (na,t)) l) b in
-	if t' == t && b' == b then c
-	else mkLambda (na, t', b')
+        if t' == t && b' == b then c
+        else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
       let b' = f (g (LocalDef (na,bo,t)) l) b in
-	if bo' == bo && t' == t && b' == b then c
-	else mkLetIn (na, bo', t', b')	    
+        if bo' == bo && t' == t && b' == b then c
+        else mkLetIn (na, bo', t', b')
   | App (c,[||]) -> assert false
   | App (t,al) ->
       (*Special treatment to be able to recognize partially applied subterms*)
@@ -629,13 +629,13 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in
       let app' = f l app in
       let a' = f l a in
-	if app' == app && a' == a then c
-	else mkApp (app', [| a' |])
+        if app' == app && a' == a then c
+        else mkApp (app', [| a' |])
   | Proj (p,b) ->
     let b' = f l b in
       if b' == b then c
       else mkProj (p, b')
-  | Evar (e,al) -> 
+  | Evar (e,al) ->
     let al' = Array.map_left (f l) al in
       if Array.for_all2 (==) al' al then c
       else mkEvar (e, al')
@@ -644,20 +644,20 @@ let map_constr_with_binders_left_to_right sigma g f l c =
       let b' = f l b in
       let p' = f l p in
       let bl' = Array.map_left (f l) bl in
-	if b' == b && p' == p && bl' == bl then c
-	else mkCase (ci, p', b', bl')
+        if b' == b && p' == p && bl' == bl then c
+        else mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
-	if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
-	then c
-	else mkFix (ln,(lna,tl',bl'))
+        if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+        then c
+        else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
-	if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
-	then c
-	else mkCoFix (ln,(lna,tl',bl'))
+        if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+        then c
+        else mkCoFix (ln,(lna,tl',bl'))
 
 let map_under_context_with_full_binders sigma g f l n d =
   let open EConstr in
@@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   let open EConstr in
   match EConstr.kind sigma cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _ | Int _) -> cstr
+    | Construct _ | Int _ | Float _) -> cstr
   | Cast (c,k, t) ->
       let c' = f l c in
       let t' = f l t in
@@ -703,9 +703,9 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
       let c' = f l c in
       let al' = Array.map (f l) al in
       if c==c' && Array.for_all2 (==) al al' then cstr else mkApp (c', al')
-  | Proj (p,c) -> 
+  | Proj (p,c) ->
       let c' = f l c in
-	if c' == c then cstr else mkProj (p, c')
+        if c' == c then cstr else mkProj (p, c')
   | Evar (e,al) ->
       let al' = Array.map (f l) al in
       if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
@@ -867,14 +867,14 @@ let dependent_main noevar sigma m t =
       raise Occur
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
-	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+        | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+            deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
             Array.Fun1.iter deprec m
-	      (Array.sub lt
-		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
-	| _, Evar _ when noevar -> ()
-	| _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
+              (Array.sub lt
+                (Array.length lm) ((Array.length lt) - (Array.length lm)))
+        | _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
+        | _, Evar _ when noevar -> ()
+        | _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
   in
   try deprec m t; false with Occur -> true
 
@@ -895,14 +895,14 @@ let count_occurrences sigma m t =
       incr n
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
-	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
-	    Array.iter (countrec m)
-	      (Array.sub lt
-		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when isMeta sigma c -> ()
-	| _, Evar _ -> ()
-	| _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
+        | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+            countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+            Array.iter (countrec m)
+              (Array.sub lt
+                (Array.length lm) ((Array.length lt) - (Array.length lm)))
+        | _, Cast (c,_,_) when isMeta sigma c -> ()
+        | _, Evar _ -> ()
+        | _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
   in
   countrec m t;
   !n
@@ -949,13 +949,13 @@ let prefix_application sigma eq_fun (k,c) t =
   let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
-	let l1 = Array.length cl1
-	and l2 = Array.length cl2 in
-	if l1 <= l2
-	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
-	else
-	  None
+        let l1 = Array.length cl1
+        and l2 = Array.length cl2 in
+        if l1 <= l2
+           && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+          Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+        else
+          None
     | _ -> None
 
 let my_prefix_application sigma eq_fun (k,c) by_c t =
@@ -963,13 +963,13 @@ let my_prefix_application sigma eq_fun (k,c) by_c t =
   let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
-	let l1 = Array.length cl1
-	and l2 = Array.length cl2 in
-	if l1 <= l2
-	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
-	else
-	  None
+        let l1 = Array.length cl1
+        and l2 = Array.length cl2 in
+        if l1 <= l2
+           && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+          Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+        else
+          None
     | _ -> None
 
 (* Recognizing occurrences of a given subterm in a term: [subst_term c t]
@@ -1002,7 +1002,7 @@ let replace_term_gen sigma eq_fun c by_c in_t =
       | None ->
     (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else
       EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
-	substrec kc t)
+        substrec kc t)
   in
   substrec (0,c) in_t
 
@@ -1127,7 +1127,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
       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
+        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'
@@ -1145,9 +1145,9 @@ let split_app sigma c = match EConstr.kind sigma c with
     App(c,l) ->
       let len = Array.length l in
       if Int.equal len 0 then ([],c) else
-	let last = Array.get l (len-1) in
-	let prev = Array.sub l 0 (len-1) in
-	c::(Array.to_list prev), last
+        let last = Array.get l (len-1) in
+        let prev = Array.sub l 0 (len-1) in
+        c::(Array.to_list prev), last
   | _ -> assert false
 
 type subst = (EConstr.rel_context * EConstr.constr) Evar.Map.t
@@ -1177,15 +1177,15 @@ let filtering sigma env cv_pb c1 c2 =
         | _ -> assert false
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
-	  aux env cv_pb t1 t2;
-	  aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
+          aux env cv_pb t1 t2;
+          aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
-	  if compare_constr_univ sigma
-	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
-	  else raise CannotFilter
-	  (* TODO: le reste des binders *)
+          if compare_constr_univ sigma
+          (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+          else raise CannotFilter
+          (* TODO: le reste des binders *)
   in
   aux env cv_pb c1 c2; !evm
 
@@ -1241,18 +1241,18 @@ let rec eta_reduce_head sigma c =
   let open Vars in
   match EConstr.kind sigma c with
     | Lambda (_,c1,c') ->
-	(match EConstr.kind sigma (eta_reduce_head sigma c') with
+        (match EConstr.kind sigma (eta_reduce_head sigma c') with
            | App (f,cl) ->
                let lastn = (Array.length cl) - 1 in
                if lastn < 0 then anomaly (Pp.str "application without arguments.")
                else
                  (match EConstr.kind sigma cl.(lastn) with
                     | Rel 1 ->
-			let c' =
+                        let c' =
                           if Int.equal lastn 0 then f
-			  else mkApp (f, Array.sub cl 0 lastn)
-			in
-			if noccurn sigma 1 c'
+                          else mkApp (f, Array.sub cl 0 lastn)
+                        in
+                        if noccurn sigma 1 c'
                         then lift (-1) c'
                         else c
                     | _   -> c)
@@ -1278,9 +1278,9 @@ let assums_of_rel_context sign =
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
     | d::sign ->
-	aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
+        aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
     | [] ->
-	acc
+        acc
   in
   aux env [] (List.rev sign)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 5ed016e0d0..3546ece581 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -15,7 +15,7 @@ open Names
 open Univ
 
 module UNameMap = Names.Id.Map
-    
+
 type uinfo = {
   uname : Id.t option;
   uloc : Loc.t option;
@@ -34,6 +34,7 @@ type t =
    (** The subset of unification variables that can be instantiated with
         algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
@@ -47,6 +48,7 @@ let empty =
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
     uctx_universes = initial_sprop_cumulative;
+    uctx_universes_lbound = Univ.Level.set;
     uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
@@ -54,10 +56,12 @@ let elaboration_sprop_cumul =
   Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
     ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
 
-let make u =
+let make ~lbound u =
   let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
-    { empty with 
-      uctx_universes = u; uctx_initial_universes = u}
+    { empty with
+      uctx_universes = u;
+      uctx_universes_lbound = lbound;
+      uctx_initial_universes = u}
 
 let is_empty ctx =
   ContextSet.is_empty ctx.uctx_local &&
@@ -83,22 +87,23 @@ let union ctx ctx' =
     let newus = LSet.diff newus (LMap.domain ctx.uctx_univ_variables) in
     let weak = UPairSet.union ctx.uctx_weak_constraints ctx'.uctx_weak_constraints in
     let declarenew g =
-      LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
+      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.uctx_universes_lbound ~strict:false g) newus g
     in
     let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
         uctx_local = local;
         uctx_seff_univs = seff;
-        uctx_univ_variables = 
+        uctx_univ_variables =
           LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
-        uctx_univ_algebraic = 
+        uctx_univ_algebraic =
           LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
         uctx_initial_universes = declarenew ctx.uctx_initial_universes;
-        uctx_universes = 
+        uctx_universes =
           (if local == ctx.uctx_local then ctx.uctx_universes
            else
              let cstrsr = ContextSet.constraints ctx'.uctx_local in
              UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes));
+        uctx_universes_lbound = ctx.uctx_universes_lbound;
         uctx_weak_constraints = weak}
 
 let context_set ctx = ctx.uctx_local
@@ -173,6 +178,7 @@ exception UniversesDiffer
 
 let drop_weak_constraints = ref false
 
+
 let process_universe_constraints ctx cstrs =
   let open UnivSubst in
   let open UnivProblem in
@@ -228,25 +234,24 @@ let process_universe_constraints ctx cstrs =
   let unify_universes cst local =
     let cst = nf_constraint cst in
       if UnivProblem.is_trivial cst then local
-      else 
+      else
           match cst with
           | ULe (l, r) ->
-            if UGraph.check_leq univs l r then
-              (* Keep Prop/Set <= var around if var might be instantiated by prop or set
-                 later. *)
-              match Universe.level l, Universe.level r with
-              | Some l, Some r ->
-                Constraint.add (l, Le, r) local
-              | _ -> local
-            else
-              begin match Universe.level r with
-              | None -> user_err Pp.(str "Algebraic universe on the right")
-              | Some r' ->
-                if Level.is_small r' then
+            begin match Univ.Universe.level r with
+            | None ->
+              if UGraph.check_leq univs l r then local
+              else user_err Pp.(str "Algebraic universe on the right")
+            | Some r' ->
+              if Level.is_small r' then
                   if not (Universe.is_levels l)
-                  then
+                  then (* l contains a +1 and r=r' small so l <= r impossible *)
                     raise (UniverseInconsistency (Le, l, r, None))
                   else
+                    if UGraph.check_leq univs l r then match Univ.Universe.level l with
+                    | Some l ->
+                      Univ.Constraint.add (l, Le, r') local
+                    | None -> local
+                    else
                     let levels = Universe.levels l in
                     let fold l' local =
                       let l = Universe.make l' in
@@ -255,8 +260,12 @@ let process_universe_constraints ctx cstrs =
                       else raise (UniverseInconsistency (Le, l, r, None))
                     in
                     LSet.fold fold levels local
-                else
-                  enforce_leq l r local
+              else
+                match Univ.Universe.level l with
+                | Some l ->
+                  Univ.Constraint.add (l, Le, r') local
+                | None ->
+                  if UGraph.check_leq univs l r then local else enforce_leq l r local
               end
           | ULub (l, r) ->
               equalize_variables true (Universe.make l) l (Universe.make r) r local
@@ -264,7 +273,7 @@ let process_universe_constraints ctx cstrs =
             if not !drop_weak_constraints then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
   in
-  let local = 
+  let local =
     UnivProblem.Set.fold unify_universes cstrs Constraint.empty
   in
     !vars, !weak, local
@@ -317,9 +326,9 @@ let constrain_variables diff ctx =
       diff (univs, ctx.uctx_univ_variables, local)
   in
   { ctx with uctx_local = (univs, local); uctx_univ_variables = vars }
-  
+
 let qualid_of_level uctx =
-  let map, map_rev = uctx.uctx_names in 
+  let map, map_rev = uctx.uctx_names in
     fun l ->
       try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
       with Not_found | Option.IsNone ->
@@ -431,18 +440,19 @@ let check_univ_decl ~poly uctx decl =
       (ContextSet.constraints uctx.uctx_local);
   ctx
 
-let restrict_universe_context (univs, csts) keep =
+let restrict_universe_context ~lbound (univs, csts) keep =
   let removed = LSet.diff univs keep in
   if LSet.is_empty removed then univs, csts
   else
   let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
   let g = UGraph.initial_universes in
-  let g = LSet.fold (fun v g -> if Level.is_small v then g else UGraph.add_universe v false g) allunivs g in
+  let g = LSet.fold (fun v g -> if Level.is_small v then g else
+                        UGraph.add_universe v ~lbound ~strict:false g) allunivs g in
   let g = UGraph.merge_constraints csts g in
   let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
   let csts = Constraint.filter (fun (l,d,r) ->
-      not ((Level.is_set l && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+      not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
 let restrict ctx vars =
@@ -450,18 +460,10 @@ let restrict ctx vars =
   let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars)
       (fst ctx.uctx_names) vars
   in
-  let uctx' = restrict_universe_context ctx.uctx_local vars in
+  let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
-let demote_seff_univs universes uctx =
-  let open Entries in
-  match universes with
-  | Polymorphic_entry _ -> uctx
-  | Monomorphic_entry (univs, _) ->
-    let seff = LSet.union uctx.uctx_seff_univs univs in
-    { uctx with uctx_seff_univs = seff }
-
-type rigid = 
+type rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -475,10 +477,9 @@ let univ_flexible_alg = UnivFlexible true
     context we merge comes from a side effect that is already inlined
     or defined separately. In the later case, there is no extension,
     see [emit_side_effects] for example. *)
-let merge ?loc ~sideff ~extend rigid uctx ctx' =
+let merge ?loc ~sideff rigid uctx ctx' =
   let levels = ContextSet.levels ctx' in
   let uctx =
-    if not extend then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
@@ -487,25 +488,23 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
         else LMap.add u None accu
       in
       let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
-        if b then
-          { uctx with uctx_univ_variables = uvars';
-          uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
-        else { uctx with uctx_univ_variables = uvars' }
+      if b then
+        { uctx with uctx_univ_variables = uvars';
+                    uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
+      else { uctx with uctx_univ_variables = uvars' }
   in
-  let uctx_local =
-    if not extend then uctx.uctx_local
-    else ContextSet.append ctx' uctx.uctx_local in
+  let uctx_local = ContextSet.append ctx' uctx.uctx_local in
   let declare g =
     LSet.fold (fun u g ->
-               try UGraph.add_universe u false g
-               with UGraph.AlreadyDeclared when sideff -> g)
-              levels g
+        try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
+        with UGraph.AlreadyDeclared when sideff -> g)
+      levels g
   in
   let uctx_names =
     let fold u accu =
       let modify _ info = match info.uloc with
-      | None -> { info with uloc = loc }
-      | Some _ -> info
+        | None -> { info with uloc = loc }
+        | Some _ -> info
       in
       try LMap.modify u modify accu
       with Not_found -> LMap.add u { uname = None; uloc = loc } accu
@@ -521,9 +520,36 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
 let merge_subst uctx s =
   { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s }
 
+let demote_seff_univs univs uctx =
+  let seff = LSet.union uctx.uctx_seff_univs univs in
+  { uctx with uctx_seff_univs = seff }
+
+let merge_seff uctx ctx' =
+  let levels = ContextSet.levels ctx' in
+  let declare g =
+    LSet.fold (fun u g ->
+        try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
+        with UGraph.AlreadyDeclared -> g)
+      levels g
+  in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare uctx.uctx_universes in
+  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+  { uctx with uctx_universes;
+              uctx_initial_universes = initial }
+
 let emit_side_effects eff u =
-  let uctxs = Safe_typing.universes_of_private eff in
-  List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
+  let uctx = Safe_typing.universes_of_private eff in
+  let u = demote_seff_univs (fst uctx) u in
+  merge_seff u uctx
+
+let update_sigma_env uctx env =
+  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
+  let eunivs =
+    { uctx with uctx_initial_universes = univs;
+                uctx_universes = univs }
+  in
+  merge_seff eunivs eunivs.uctx_local
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
@@ -532,28 +558,29 @@ let new_univ_variable ?loc rigid name
   let uctx', pred =
     match rigid with
     | UnivRigid -> uctx, true
-    | UnivFlexible b -> 
+    | UnivFlexible b ->
       let uvars' = LMap.add u None uvars in
         if b then {uctx with uctx_univ_variables = uvars';
           uctx_univ_algebraic = LSet.add u avars}, false
         else {uctx with uctx_univ_variables = uvars'}, false
   in
-  let names = 
+  let names =
     match name with
     | Some n -> add_uctx_names ?loc n u uctx.uctx_names
     | None -> add_uctx_loc u loc uctx.uctx_names
   in
   let initial =
-    UGraph.add_universe u false uctx.uctx_initial_universes
-  in                                                 
+    UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u uctx.uctx_initial_universes
+  in
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-                uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
+                uctx_universes = UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false
+                    u uctx.uctx_universes;
                 uctx_initial_universes = initial}
   in uctx', u
 
-let make_with_initial_binders e us =
-  let uctx = make e in
+let make_with_initial_binders ~lbound e us =
+  let uctx = make ~lbound e in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
@@ -561,10 +588,10 @@ let make_with_initial_binders e us =
 
 let add_global_univ uctx u =
   let initial =
-    UGraph.add_universe u true uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
   in
-  let univs = 
-    UGraph.add_universe u true uctx.uctx_universes
+  let univs =
+    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
   in
   { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
                                      uctx_initial_universes = initial;
@@ -604,11 +631,11 @@ let make_nonalgebraic_variable ctx u =
 let make_flexible_nonalgebraic ctx =
   {ctx with uctx_univ_algebraic = LSet.empty}
 
-let is_sort_variable uctx s = 
-  match s with 
-  | Sorts.Type u -> 
+let is_sort_variable uctx s =
+  match s with
+  | Sorts.Type u ->
     (match universe_level u with
-    | Some l as x -> 
+    | Some l as x ->
         if LSet.mem l (ContextSet.levels uctx.uctx_local) then x
         else None
     | None -> None)
@@ -646,7 +673,7 @@ let normalize_variables uctx =
       uctx_universes = univs }
 
 let abstract_undefined_variables uctx =
-  let vars' = 
+  let vars' =
     LMap.fold (fun u v acc ->
       if v == None then LSet.remove u acc
       else acc)
@@ -655,11 +682,11 @@ let abstract_undefined_variables uctx =
       uctx_univ_algebraic = vars' }
 
 let fix_undefined_variables uctx =
-  let algs', vars' = 
+  let algs', vars' =
     LMap.fold (fun u v (algs, vars as acc) ->
       if v == None then (LSet.remove u algs, LMap.remove u vars)
       else acc)
-      uctx.uctx_univ_variables 
+      uctx.uctx_univ_variables
       (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
   in
   { uctx with uctx_univ_variables = vars';
@@ -671,7 +698,7 @@ let refresh_undefined_univ_variables uctx =
   let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
     uctx.uctx_univ_algebraic LSet.empty
   in
-  let vars = 
+  let vars =
     LMap.fold
       (fun u v acc ->
         LMap.add (subst_fn u)
@@ -679,8 +706,9 @@ let refresh_undefined_univ_variables uctx =
       uctx.uctx_univ_variables LMap.empty
   in
   let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.uctx_weak_constraints UPairSet.empty in
-  let declare g = LSet.fold (fun u g -> UGraph.add_universe u false g)
-                                   (ContextSet.levels ctx') g in
+  let lbound = uctx.uctx_universes_lbound in
+  let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
+      (ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
@@ -688,14 +716,16 @@ let refresh_undefined_univ_variables uctx =
                uctx_seff_univs = uctx.uctx_seff_univs;
                uctx_univ_variables = vars; uctx_univ_algebraic = alg;
                uctx_universes = univs;
+               uctx_universes_lbound = lbound;
                uctx_initial_universes = initial;
                uctx_weak_constraints = weak; } in
     uctx', subst
 
 let minimize uctx =
   let open UnivMinim in
+  let lbound = uctx.uctx_universes_lbound in
   let ((vars',algs'), us') =
-    normalize_context_set uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
+    normalize_context_set ~lbound uctx.uctx_universes uctx.uctx_local uctx.uctx_univ_variables
       uctx.uctx_univ_algebraic uctx.uctx_weak_constraints
   in
   if ContextSet.equal us' uctx.uctx_local then uctx
@@ -706,23 +736,16 @@ let minimize uctx =
       { uctx_names = uctx.uctx_names;
         uctx_local = us';
         uctx_seff_univs = uctx.uctx_seff_univs; (* not sure about this *)
-        uctx_univ_variables = vars'; 
+        uctx_univ_variables = vars';
         uctx_univ_algebraic = algs';
         uctx_universes = universes;
+        uctx_universes_lbound = lbound;
         uctx_initial_universes = uctx.uctx_initial_universes;
         uctx_weak_constraints = UPairSet.empty; (* weak constraints are consumed *) }
 
-let universe_of_name uctx s = 
+let universe_of_name uctx s =
   UNameMap.find s (fst uctx.uctx_names)
 
-let update_sigma_env uctx env =
-  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
-  let eunivs =
-    { uctx with uctx_initial_universes = univs;
-                         uctx_universes = univs }
-  in
-  merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
-
 let pr_weak prl {uctx_weak_constraints=weak} =
   let open Pp in
   prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
diff --git a/engine/uState.mli b/engine/uState.mli
index 9689f2e961..8855a6bea6 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
 
 val empty : t
 
-val make : UGraph.t -> t
+val make : lbound:Univ.Level.t -> UGraph.t -> t
 
-val make_with_initial_binders : UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -88,11 +88,11 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
 
 (** {5 Unification} *)
 
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
@@ -100,9 +100,7 @@ val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
    universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
-val demote_seff_univs : Entries.universes_entry -> t -> t
-
-type rigid = 
+type rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -110,10 +108,15 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
 val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
+val demote_seff_univs : Univ.LSet.t -> t -> t
+(** Mark the universes as not local any more, because they have been
+   globally declared by some side effect. You should be using
+   emit_side_effects instead. *)
+
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t
 
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b1ed3b2694..1fe09270ba 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -82,14 +82,6 @@ let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
   | IsGlobal gr -> fresh_global_instance env gr
 
-let global_of_constr c =
-  match kind c with
-  | Const (c, u) -> GlobRef.ConstRef c, u
-  | Ind (i, u) -> GlobRef.IndRef i, u
-  | Construct (c, u) -> GlobRef.ConstructRef c, u
-  | Var id -> GlobRef.VarRef id, Instance.empty
-  | _ -> raise Not_found
-
 let fresh_sort_in_family = function
   | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 1c8735bfa8..1b351c61c4 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -54,9 +54,6 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const
 val fresh_universe_context_set_instance : ContextSet.t ->
   universe_level_subst * ContextSet.t
 
-(** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> GlobRef.t puniverses
-
 (** Create a fresh global in the global environment, without side effects.
     BEWARE: this raises an error on polymorphic constants/inductives:
     the constraints should be properly added to an evd.
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1b7c33b9c1..30fdd28997 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -269,11 +269,11 @@ module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
 (* TODO check is_small/sprop *)
-let normalize_context_set g ctx us algs weak =
+let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
@@ -282,12 +282,12 @@ let normalize_context_set g ctx us algs weak =
   let csts, partition =
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = LSet.fold (fun v g -> UGraph.add_universe v false g)
+    let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g)
                            ctx UGraph.initial_universes
     in
     let add_soft u g =
       if not (Level.is_small u || LSet.mem u ctx)
-      then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g
+      then try UGraph.add_universe ~lbound ~strict:false u g with UGraph.AlreadyDeclared -> g
       else g
     in
     let g = Constraint.fold
@@ -300,7 +300,7 @@ let normalize_context_set g ctx us algs weak =
   (* We ignore the trivial Prop/Set <= i constraints. *)
   let noneqs =
     Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.is_small l) ||
+      (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
                            (Level.is_prop l && d == Lt && Level.is_set r)))
       csts
   in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 21f6efe86a..72b432e62f 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
   LSet.t (* univ variables that can be substituted by algebraics *) ->
   UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 6cc7868a38..1f1edbed16 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
 [@@ocaml.deprecated "Use [UState.restrict_universe_context]"]