diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 1575616ff39e..d62249f42226 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -53,6 +53,25 @@ let default_case_analysis_dependence env ind =
 (*             Induction/recursion schemes              *)
 (* **************************************************** *)
 
+let build_induction_scheme_in_sort_var env dep ind =
+  let sigma = Evd.from_env env in
+  let sigma, pind =
+    Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind
+  in
+  (* Get new sort for output *)
+  let sigma, pred_sort = Evd.new_sort_variable UnivRigid sigma in
+  let pred_quality = EConstr.ESorts.quality sigma pred_sort in
+  (* Get sort of inductive *)
+  let _, ind_sort =
+    EConstr.destArity sigma
+      (Retyping.get_type_of env sigma (EConstr.mkIndU pind))
+  in
+  let ind_quality = EConstr.ESorts.quality sigma ind_sort in
+  (* Set elimination constraint from inductive to output's sort *)
+  let sigma = Evd.set_elim_to sigma ind_quality pred_quality in
+  let sigma, c = build_induction_scheme env sigma pind dep pred_sort in
+  (EConstr.to_constr sigma c, Evd.ustate sigma)
+
 let build_induction_scheme_in_type env dep sort ind =
   let sigma = Evd.from_env env in
   let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
@@ -76,6 +95,10 @@ let sind_dep =
   declare_individual_scheme_object "sind_dep"
     (fun env _ x -> build_induction_scheme_in_type env true QualityOrSet.sprop x)
 
+let poly_dep =
+  declare_individual_scheme_object "poly_dep"
+    (fun env _ x -> build_induction_scheme_in_sort_var env true x)
+
 let rect_nodep =
   declare_individual_scheme_object "rect_nodep"
     (fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.qtype x)
@@ -92,6 +115,10 @@ let sind_nodep =
   declare_individual_scheme_object "sind_nodep"
     (fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.sprop x)
 
+let poly_nodep =
+  declare_individual_scheme_object "poly_nodep"
+    (fun env _ x -> build_induction_scheme_in_sort_var env false x)
+
 let elim_scheme ~dep ~to_kind =
   let open QualityOrSet in
   match to_kind with
@@ -100,10 +127,12 @@ let elim_scheme ~dep ~to_kind =
        match q with
        | QConstant QSProp when dep -> sind_dep
        | QConstant QProp when dep -> ind_dep
-       | (QConstant QType | QVar _) when dep -> rect_dep
+       | QConstant QType when dep -> rect_dep
+       | Sorts.Quality.QVar _ when dep -> poly_dep
        | QConstant QSProp -> sind_nodep
        | QConstant QProp -> ind_nodep
-       | QConstant QType | QVar _ -> rect_nodep
+       | QConstant QType -> rect_nodep
+       | Sorts.Quality.QVar _ -> poly_nodep
      end
   | Set -> if dep then rec_dep else rec_nodep
 
@@ -199,6 +228,14 @@ let case_nodep =
   declare_individual_scheme_object "case_nodep"
     (fun env _ x -> build_case_analysis_scheme_in_type env false QualityOrSet.qtype x)
 
+let case_poly_dep q =
+  declare_individual_scheme_object "case_poly_dep"
+    (fun env _ x -> build_case_analysis_scheme_in_type env true (QualityOrSet.Qual q) x)
+
+let case_poly_nodep q =
+  declare_individual_scheme_object "case_poly_nodep"
+    (fun env _ x -> build_case_analysis_scheme_in_type env false (QualityOrSet.Qual q) x)
+
 let casep_dep =
   declare_individual_scheme_object "casep_dep"
     (fun env _ x -> build_case_analysis_scheme_in_type env true QualityOrSet.prop x)
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index 311c4aedc0f2..35d8a77c732e 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -36,6 +36,8 @@ val elim_scheme : dep:bool -> to_kind:UnivGen.QualityOrSet.t -> individual schem
 val case_dep : individual scheme_kind
 val case_nodep : individual scheme_kind
 val casep_dep : individual scheme_kind
+val case_poly_dep : Sorts.Quality.t -> individual scheme_kind
+val case_poly_nodep : Sorts.Quality.t -> individual scheme_kind
 val casep_nodep : individual scheme_kind
 
 (** Recursor names utilities *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 7390bfcf545c..d4a74ed6f36f 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -218,45 +218,61 @@ let declare_one_case_analysis_scheme ?loc ind =
 
 (* Induction/recursion schemes *)
 
-let declare_one_induction_scheme ?loc ind =
-  let (mib,mip) as specif = Global.lookup_inductive ind in
-  let kind = Elimschemes.pseudo_sort_quality_for_elim ind mip in
-  let from_prop = Sorts.Quality.is_qprop kind in
-  let depelim = Inductiveops.has_dependent_elim specif in
-  let kelim mip = Inductiveops.constant_sorts_below
-              @@ Inductiveops.elim_sort (mib,mip) in
-  let kelim =
-    List.fold_right (fun x acc ->
-      List.intersect UnivGen.QualityOrSet.equal acc x)
-    (List.map kelim (Array.to_list mib.mind_packets))
-    [UnivGen.QualityOrSet.qtype; UnivGen.QualityOrSet.prop; UnivGen.QualityOrSet.set; UnivGen.QualityOrSet.sprop] in
-  let kelim =
-    if Global.sprop_allowed ()
-    then kelim
-    else List.filter (fun s -> not (UnivGen.QualityOrSet.is_sprop s)) kelim
-  in
-  let elims =
-    List.filter (fun (sort,_) -> List.mem_f UnivGen.QualityOrSet.equal sort kelim)
-      [(UnivGen.QualityOrSet.qtype, "rect");
-       (UnivGen.QualityOrSet.prop, "ind");
-       (UnivGen.QualityOrSet.set, "rec");
-       (UnivGen.QualityOrSet.sprop, "sind")]
+let declare_one_induction_scheme_poly ?loc ind (mib, mip) q =
+  let scheme_kind =
+    elim_scheme ~dep:true ~to_kind:(UnivGen.QualityOrSet.Qual q)
   in
-  let elims = List.map (fun (to_kind,dflt_suff) ->
-      if from_prop then elim_scheme ~dep:false ~to_kind, Some dflt_suff
-      else if depelim then elim_scheme ~dep:true ~to_kind, Some dflt_suff
-      else elim_scheme ~dep:false ~to_kind, None)
+  let suff = "_poly_rec" in
+  let id = Some Names.(Id.of_string (Id.to_string mip.mind_typename ^ suff)) in
+  define_individual_scheme ?loc scheme_kind id ind
+
+let declare_one_induction_scheme_const ?loc ind (mib, mip as specif) kind =
+    let from_prop = Sorts.Quality.is_qprop kind in
+    let depelim = Inductiveops.has_dependent_elim specif in
+    let kelim mip = Inductiveops.constant_sorts_below
+      @@ Inductiveops.elim_sort (mib,mip) in
+    let kelim =
+      List.fold_right (fun x acc ->
+          List.intersect UnivGen.QualityOrSet.equal acc x)
+        (List.map kelim (Array.to_list mib.mind_packets))
+        [UnivGen.QualityOrSet.qtype; UnivGen.QualityOrSet.prop; UnivGen.QualityOrSet.set; UnivGen.QualityOrSet.sprop] in
+    let kelim =
+      if Global.sprop_allowed ()
+      then kelim
+      else List.filter (fun s -> not (UnivGen.QualityOrSet.is_sprop s)) kelim
+    in
+    let elims =
+      List.filter (fun (sort, _) -> List.mem_f UnivGen.QualityOrSet.equal sort kelim)
+        (* NB: the order is important, it makes it so that _rec is
+           defined using _rect but _ind is not. *)
+        [(UnivGen.QualityOrSet.qtype, "rect");
+         (UnivGen.QualityOrSet.prop, "ind");
+         (UnivGen.QualityOrSet.set, "rec");
+         (UnivGen.QualityOrSet.sprop, "sind")]
+    in
+    let elims = List.map (fun (to_kind, dflt_suff) ->
+        if from_prop then elim_scheme ~dep:false ~to_kind, Some dflt_suff
+        else if depelim then elim_scheme ~dep:true ~to_kind, Some dflt_suff
+        else elim_scheme ~dep:false ~to_kind, None)
+        elims
+    in
+    List.iter (fun (kind, suff) ->
+        let id = match suff with
+          | None -> None
+          | Some suff ->
+            (* the auto generated eliminator may be called "rect" instead of eg "rect_dep" *)
+            Some Names.(Id.of_string (Id.to_string mip.mind_typename ^ "_" ^ suff))
+        in
+        define_individual_scheme ?loc kind id ind)
       elims
-  in
-  List.iter (fun (kind, suff) ->
-      let id = match suff with
-        | None -> None
-        | Some suff ->
-          (* the auto generated eliminator may be called "rect" instead of eg "rect_dep" *)
-          Some Names.(Id.of_string (Id.to_string mip.mind_typename ^ "_" ^ suff))
-      in
-      define_individual_scheme ?loc kind id ind)
-         elims
+
+let declare_one_induction_scheme ?loc ind =
+  let ((mib, mip) as specif) = Global.lookup_inductive ind in
+  let quality = Elimschemes.pseudo_sort_quality_for_elim ind mip in
+  if Sorts.Quality.is_qvar quality then
+    declare_one_induction_scheme_poly ?loc ind specif quality
+  else
+    declare_one_induction_scheme_const ?loc ind specif quality
 
 let declare_induction_schemes ?(locmap=Locmap.default None) kn =
   let mib = Global.lookup_mind kn in
@@ -414,7 +430,8 @@ let do_mutual_induction_scheme ~register ?(force_mutual=false) env ?(isrec=true)
       else match sort with
         | Qual (QConstant QType) -> Some (if dep then case_dep else case_nodep)
         | Qual (QConstant QProp) -> Some (if dep then casep_dep else casep_nodep)
-        | Set | Qual (QConstant QSProp | QVar _) ->
+        | Qual (QVar _ as q) -> Some (if dep then case_poly_dep q else case_poly_nodep q)
+        | Set | Qual (QConstant QSProp) ->
           (* currently we don't have standard scheme kinds for this *)
           None
     in