4 files changed, 14 insertions, 19 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 8e7d942c37..70f58163fd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u =
 let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
   with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
 
-let fresh_constant_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
+let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c =
+  with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c)
 
-let fresh_inductive_instance ?loc env evd i =
-  with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
+let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i =
+  with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i)
 
-let fresh_constructor_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
+let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
+  with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
   with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
diff --git a/engine/evd.mli b/engine/evd.mli
index 8843adc853..82e1003a65 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map
 
 (** Polymorphic universes *)
 
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
-val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
-val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid
+  -> evar_map -> Sorts.family -> evar_map * Sorts.t
+val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid
+  -> env -> evar_map -> Constant.t -> evar_map * pconstant
+val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
+  -> env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid
+  -> env -> evar_map -> constructor -> evar_map * pconstructor
 
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
   evar_map -> GlobRef.t -> evar_map * econstr
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 1fe09270ba..b270f9dc0b 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function
 
 (** Fresh universe polymorphic construction *)
 
-open Globnames
-
 let fresh_global_instance ?loc ?names env gr =
   let auctx = Environ.universes_of_global env gr in
   let u, ctx = fresh_instance_from ?loc auctx names in
@@ -78,10 +76,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 fresh_global_or_constr_instance env = function
-  | IsConstr c -> c, ContextSet.empty
-  | IsGlobal gr -> fresh_global_instance env gr
-
 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 1b351c61c4..bbde9d4e30 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor ->
 val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
   constr in_universe_context_set
 
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
-  constr in_universe_context_set
-
 (** Get fresh variables for the universe context.
     Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
 val fresh_universe_context_set_instance : ContextSet.t ->