Merge PR #11419: schemes: use rigid universes

Reviewed-by: ppedrot

4 files changed, 21 insertions, 12 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/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
 
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index 855f26698c..4b928007cf 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep.
 Set Rewriting Schemes.
 Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
 Unset Rewriting Schemes.
+
+(* check that the scheme doesn't minimize itself into something non general *)
+Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
+Lemma bla@{u v|u < v} : foo@{u v} -> False.
+Proof. induction 1. Qed.