Merge remote-tracking branch 'origin/master' into stm+doc_hook

15 files changed, 49 insertions, 218 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 96beb72a56..0a5bba39b9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -26,24 +26,7 @@ let safe_evar_value sigma ev =
   try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
-(** Combinators *)
-
-let evd_comb0 f evdref =
-  let (evd',x) = f !evdref in
-    evdref := evd';
-    x
-
-let evd_comb1 f evdref x =
-  let (evd',y) = f !evdref x in
-    evdref := evd';
-    y
-
-let evd_comb2 f evdref x y =
-  let (evd',z) = f !evdref x y in
-    evdref := evd';
-    z
-
-let new_global evd x = 
+let new_global evd x =
   let (evd, c) = Evd.fresh_global (Global.env()) evd x in
   (evd, c)
 
@@ -673,26 +656,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 q is_dependent c =
-  queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
+let queue_term evm q is_dependent c =
+  queue_set q is_dependent (evars_of_term evm 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 q true evi.evar_concl;
+  queue_term evm q true evi.evar_concl;
   List.iter begin fun decl ->
     let open NamedDecl in
-    queue_term q true (NamedDecl.get_type decl);
+    queue_term evm q true (NamedDecl.get_type decl);
     match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> queue_term q true b
+    | LocalDef (_,b,_) -> queue_term evm 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 (EConstr.Unsafe.to_constr b) in
+      let subevars = evars_of_term evm 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
@@ -812,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
   in
   let accu = match evi.evar_body with
   | Evar_empty -> Evar.Set.empty
-  | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
+  | Evar_defined b -> evars_of_term sigma b
   in
   let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
   let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index bb0da44103..8eaff8bd13 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -274,15 +274,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-
 val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b89222cf8e..15b4c31851 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -222,7 +222,7 @@ let map_evar_body f = function
 let map_evar_info f evi =
   {evi with
     evar_body = map_evar_body f evi.evar_body;
-    evar_hyps = map_named_val f evi.evar_hyps;
+    evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps;
     evar_concl = f evi.evar_concl;
     evar_candidates = Option.map (List.map f) evi.evar_candidates }
 
@@ -823,33 +823,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _             -> None
 
-(** The following functions return the set of evars immediately
-    contained in the object *)
-
-(* excluding defined evars *)
-
-let evars_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
-  evrec Evar.Set.empty c
-
-let evars_of_named_context nc =
-  Context.Named.fold_outside
-    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr)))
-    nc
-    ~init:Evar.Set.empty
-
-let evars_of_filtered_evar_info evi =
-  Evar.Set.union (evars_of_term evi.evar_concl)
-    (Evar.Set.union
-	(match evi.evar_body with
-	| Evar_empty -> Evar.Set.empty
-	| Evar_defined b -> evars_of_term b)
-	(evars_of_named_context (evar_filtered_context evi)))
-
 (**********************************************************)
 (* Sort variables *)
 
@@ -869,8 +842,6 @@ let to_universe_context evd = UState.context evd.universes
 
 let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
 
-let const_univ_entry = univ_entry
-
 let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
 let restrict_universe_context evd vars =
@@ -1406,3 +1377,30 @@ module MiniEConstr = struct
   let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
 
 end
+
+(** The following functions return the set of evars immediately
+    contained in the object *)
+
+(* excluding defined evars *)
+
+let evars_of_term evd c =
+  let rec evrec acc c =
+    match MiniEConstr.kind evd 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 evars_of_named_context evd nc =
+  Context.Named.fold_outside
+    (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr)))
+    nc
+    ~init:Evar.Set.empty
+
+let evars_of_filtered_evar_info evd evi =
+  Evar.Set.union (evars_of_term evd evi.evar_concl)
+    (Evar.Set.union
+       (match evi.evar_body with
+       | Evar_empty -> Evar.Set.empty
+       | Evar_defined b -> evars_of_term evd b)
+       (evars_of_named_context evd (evar_filtered_context evi)))
diff --git a/engine/evd.mli b/engine/evd.mli
index b0fcddb068..587a1de044 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map ->
 val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
 val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
 
-(** The following functions return the set of evars immediately
-    contained in the object; need the term to be evar-normal otherwise
-    defined evars are returned too. *)
+(** The following functions return the set of undefined evars
+    contained in the object. *)
 
-val evars_of_term : constr -> Evar.Set.t
+val evars_of_term : evar_map -> econstr -> Evar.Set.t
   (** including evars in instances of evars *)
 
-val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
+val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
 
-val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
+val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 (** Metas *)
 val meta_list : evar_map -> (metavariable * clbinding) list
@@ -615,9 +614,6 @@ val to_universe_context : evar_map -> Univ.UContext.t
 
 val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
 
-val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
 val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index ac0344148a..dab2e7d5ef 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
 
 let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
 
-let nf_enter f =
-  bind goals
-    (fun gl ->
-      gl >>= fun gl ->
-      Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
-
 let enter f =
   bind goals
     (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 3c4fa6f4e8..ed95d62bc6 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -41,9 +41,6 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 
 (** {5 Focussing} *)
 
-val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
-[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
-
 (** Enter a goal. The resulting tactic is focussed. *)
 
 val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..5c5a02d3fa 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -46,7 +46,7 @@ let compact el ({ solution } as pv) =
   let apply_subst_einfo _ ei =
     Evd.({ ei with
        evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps;
        evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
@@ -641,7 +641,7 @@ let shelve_goals l =
     [sigma]. *)
 let depends_on sigma src tgt =
   let evi = Evd.find sigma tgt in
-  Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+  Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi))
 
 let unifiable_delayed g l =
   CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
@@ -1104,13 +1104,6 @@ module Goal = struct
         tclZERO ~info e
     end
     end
-
-  let normalize { self; state } =
-    Env.get >>= fun env ->
-    tclEVARMAP >>= fun sigma ->
-    let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
-    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
   let gmake env sigma goal =
     let state = get_state goal in
     let goal = drop_state goal in
@@ -1258,9 +1251,9 @@ module V82 = struct
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }
 
-  let top_evars initial =
+  let top_evars initial { solution=sigma; } =
     let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+      Evar.Set.elements (Evd.evars_of_term sigma c)
     in
     CList.flatten (CList.map evars_of_initial initial)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 9455dae643..b7ff3ac432 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -505,10 +505,6 @@ module Goal : sig
   (** Type of goals. *)
   type t
 
-  (** Normalises the argument goal. *)
-  val normalize : t -> t tactic
-  [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
-
   (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
@@ -599,7 +595,7 @@ module V82 : sig
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
 
   (* returns the existential variable used to start the proof *)
-  val top_evars : entry -> Evar.t list
+  val top_evars : entry -> proofview -> Evar.t list
 
   (* Caution: this function loses quite a bit of information. It
      should be avoided as much as possible.  It should work as
diff --git a/engine/termops.ml b/engine/termops.ml
index 8e12c9be88..fcacb53ac4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration
 
 module Internal = struct
 
-let pr_sort_family = Sorts.pr_sort_family
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-let pr_fix = Constr.debug_print_fix
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
 let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
 let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
 let term_printer = ref debug_print_constr_env
@@ -192,7 +187,7 @@ let compute_evar_dependency_graph sigma =
     in
     match evar_body evi with
     | Evar_empty -> acc
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc
   in
   Evd.fold fold sigma EvMap.empty
 
@@ -761,13 +756,6 @@ let fold_constr_with_binders sigma g f n acc c =
   let c = Unsafe.to_constr (whd_evar sigma c) in
   Constr.fold_constr_with_binders g f n acc c
 
-(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
-   subterms of [c]; it carries an extra data [acc] which is processed by [g] at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
-
-let iter_constr_with_full_binders = EConstr.iter_with_full_binders
-
 (***************************)
 (* occurs check functions  *)
 (***************************)
@@ -862,8 +850,6 @@ let collect_vars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
-let vars_of_global_reference = vars_of_global
-
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
@@ -1417,10 +1403,6 @@ let prod_applist_assum sigma n c l =
     | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
-let on_judgment = Environ.on_judgment
-let on_judgment_value = Environ.on_judgment_value
-let on_judgment_type = Environ.on_judgment_type
-
 (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
      variables skips let-in's; let-in's in the middle are put in ctx2 *)
 let context_chop k ctx =
diff --git a/engine/termops.mli b/engine/termops.mli
index 1dd9941c5e..a9217b3586 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -16,12 +16,6 @@ open Constr
 open Environ
 open EConstr
 
-(** printers *)
-val pr_sort_family : Sorts.family -> Pp.t
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
 (** about contexts *)
 val push_rel_assum : Name.t Context.binder_annot * types -> env -> env
 val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
@@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map ->
   ('a -> 'b -> constr -> 'b) ->
   'a -> 'b -> constr -> 'b
 
-val iter_constr_with_full_binders : Evd.evar_map ->
-  (rel_declaration -> 'a -> 'a) ->
-  ('a -> constr -> unit) -> 'a ->
-  constr -> unit
-[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
-
 (**********************************************************************)
 
 val strip_head_cast : Evd.evar_map -> constr -> constr
@@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
 
-val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
-[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
-
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
 val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
@@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool
 
 val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
 
-(** Combinators on judgments *)
-
-val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment]."]
-val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
-val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
-
 (** {5 Debug pretty-printers} *)
 
 open Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index 6f4f40e2c5..adea78d4c9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -85,7 +85,7 @@ let union ctx ctx' =
     let declarenew g =
       LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
-    let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) 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;
@@ -116,8 +116,6 @@ let univ_entry ~poly uctx =
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
-let const_univ_entry = univ_entry
-
 let of_context_set ctx = { empty with uctx_local = ctx }
 
 let subst ctx = ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index a358813825..3df7f9e8e9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t
 val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
-val const_univ_entry : poly:bool -> t -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
 (** {5 Constraints handling} *)
 
 val drop_weak_constraints : bool ref
diff --git a/engine/univGen.ml b/engine/univGen.ml
index c310331b15..f1deb1bfaf 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -25,11 +25,6 @@ let new_univ_global () =
 let fresh_level () =
   Univ.Level.make (new_univ_global ())
 
-(* TODO: remove *)
-let new_univ () = Univ.Universe.make (fresh_level ())
-let new_Type () = mkType (new_univ ())
-let new_Type_sort () = sort_of_univ (new_univ ())
-
 let fresh_instance auctx =
   let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
   let ctx = Array.fold_right LSet.add inst LSet.empty in
@@ -83,10 +78,6 @@ let constr_of_monomorphic_global gr =
       Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
           str " would forget universes.")
 
-let constr_of_global gr = constr_of_monomorphic_global gr
-
-let constr_of_global_univ = mkRef
-
 let fresh_global_or_constr_instance env = function
   | IsConstr c -> c, ContextSet.empty
   | IsGlobal gr -> fresh_global_instance env gr
@@ -99,34 +90,6 @@ let global_of_constr c =
   | Var id -> VarRef id, Instance.empty
   | _ -> raise Not_found
 
-open Declarations
-
-let type_of_reference env r =
-  match r with
-  | VarRef id -> Environ.named_type id env, ContextSet.empty
-
-  | ConstRef c ->
-     let cb = Environ.lookup_constant c env in
-     let ty = cb.const_type in
-     let auctx = Declareops.constant_polymorphic_context cb in
-     let inst, ctx = fresh_instance auctx in
-     Vars.subst_instance_constr inst ty, ctx
-
-  | IndRef ind ->
-    let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
-    let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance auctx in
-    let ty = Inductive.type_of_inductive env (specif, inst) in
-    ty, ctx
-
-  | ConstructRef (ind,_ as cstr) ->
-    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-    let auctx = Declareops.inductive_polymorphic_context mib in
-    let inst, ctx = fresh_instance auctx in
-    Inductive.type_of_constructor (cstr,inst) specif, ctx
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
 let fresh_sort_in_family = function
   | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
@@ -135,11 +98,6 @@ let fresh_sort_in_family = function
     let u = fresh_level () in
       sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
 
-let new_sort_in_family sf =
-  fst (fresh_sort_in_family sf)
-
-let extend_context = Univ.extend_in_context_set
-
 let new_global_univ () =
   let u = fresh_level () in
   (Univ.Universe.make u, ContextSet.singleton u)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index b4598e10d0..34920e5620 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *)
 val new_univ_global : unit -> Level.UGlobal.t
 val fresh_level : unit -> Level.t
 
-val new_univ : unit -> Universe.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type : unit -> types
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type_sort : unit -> Sorts.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-
 val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
 
 (** Build a fresh instance for a given context, its associated substitution and
     the instantiated constraints. *)
@@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t ->
 (** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> GlobRef.t puniverses
 
-val constr_of_global_univ : GlobRef.t puniverses -> constr
-[@@ocaml.deprecated "Use [Constr.mkRef]"]
-
-val extend_context : 'a in_universe_context_set -> ContextSet.t ->
-  'a in_universe_context_set
-[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
-
 (** 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.
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
     the proper way to get a fresh copy of a polymorphic global reference. *)
 val constr_of_monomorphic_global : GlobRef.t -> constr
-
-val constr_of_global : GlobRef.t -> constr
-[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
-                     use [constr_of_monomorphic_global] if the reference is guaranteed to\
-                     be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
-
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic
-    references and computing their instantiated universe context. (side-effect on the
-    universe counter, use with care). *)
-val type_of_global : GlobRef.t -> types in_universe_context_set
-[@@ocaml.deprecated "use [Typeops.type_of_global]"]
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 46ff6340b4..fcbf305f9d 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
           (acc, [], LMap.empty, LMap.empty) l
         in
         let left = CList.uniquize (List.filter (not_lower lower) left) in
-        (acc, left, LMap.union newlow lower)
+        (acc, left, LMap.lunion newlow lower)
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in