Adapt to rocq-prover/rocq#21820 (collapse_sort_variables arg change) (mit-plv#196)

Author: SkySkimmer

src/Rewriter/Util/plugins/inductive_from_elim.ml.v93

@@ -44,7 +44,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
     let ctor_type_to_constr cty =
       EConstr.to_constr sigma (EConstr.Vars.subst_var sigma name cty)
     in
-    let sigma = Evd.collapse_sort_variables sigma in
+    let sigma = Evd.collapse_sort_variables ~only_above_prop:false sigma in
     let univs, ubinders = Evd.check_univ_decl ~poly:PolyFlags.default sigma UState.default_univ_decl in
     let uctx = match univs with
     | UState.Monomorphic_entry ctx ->