3 files changed, 23 insertions, 8 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml
index da4de3df77..c7581fb0e0 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -130,8 +130,8 @@ let dummy_constant cst = {
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant : constant_obj -> obj) =
-  declare_object { (default_object "CONSTANT") with
+let (objConstant : constant_obj Libobject.Dyn.tag) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -139,6 +139,8 @@ let (inConstant : constant_obj -> obj) =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let inConstant v = Libobject.Dyn.Easy.inj v objConstant
+
 let update_tables c =
   Impargs.declare_constant_implicits c;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
@@ -357,12 +359,14 @@ type variable_declaration =
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
-let inVariable : unit -> obj =
-  declare_object { (default_object "VARIABLE") with
+let objVariable : unit Libobject.Dyn.tag =
+  declare_object_full { (default_object "VARIABLE") with
     classify_function = (fun () -> Dispose)}
 
+let inVariable v = Libobject.Dyn.Easy.inj v objVariable
+
 let declare_variable ~name ~kind d =
-  (* Constr raisonne sur les noms courts *)
+  (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
@@ -497,4 +501,9 @@ module Internal = struct
     ; proof_entry_type = Some typ
     }, args
 
+  type nonrec constant_obj = constant_obj
+
+  let objVariable = objVariable
+  let objConstant = objConstant
+
 end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index c646d2f85b..00c1e31717 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -131,7 +131,8 @@ val check_exists : Id.t -> unit
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)
 
-(* For legacy support, do not use *)
+(** {6 For legacy support, do not use}  *)
+
 module Internal : sig
 
   val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
@@ -145,4 +146,9 @@ module Internal : sig
 
   val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
 
+  type constant_obj
+
+  val objConstant : constant_obj Libobject.Dyn.tag
+  val objVariable : unit Libobject.Dyn.tag
+
 end
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index d6fda00ad8..6cdb24965d 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind =
     let sigma = Evd.minimize_universes sigma in
     (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
   else
-    let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+    let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
       (c, Evd.evar_universe_context sigma)
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+  let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
   let sigma, c = build_induction_scheme env sigma pind dep sort in
     c, Evd.evar_universe_context sigma