Adapt to rocq-prover/rocq#21419 (#188)

Author: mattam82

src/Rewriter/Util/plugins/definition_by_tactic.mli.v92

@@ -2,10 +2,10 @@ open Ltac_plugin
 
 val make_definition_by_tactic
   : Evd.evar_map
-  -> poly:bool
+  -> poly:PolyFlags.t
   -> Names.Id.t
   -> EConstr.t
   -> unit Proofview.tactic
   -> Names.Constant.t
 
-val vernac_make_definition_by_tactic : poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Tacexpr.raw_tactic_expr -> unit
+val vernac_make_definition_by_tactic : poly:PolyFlags.t -> Names.Id.t -> Constrexpr.constr_expr -> Tacexpr.raw_tactic_expr -> unit

src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg.v92

@@ -11,12 +11,12 @@ DECLARE PLUGIN "coq-rewriter.definition_by_tactic"
 
 VERNAC COMMAND EXTEND DefinitionViaTactic CLASSIFIED AS SIDEFF
   | [ "Make" "Definition" ":" constr(ty) ":=" tactic(tac) ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     let name = Namegen.next_global_ident_away (Global.safe_env ()) (Names.Id.of_string "Unnamed_thm") Names.Id.Set.empty in
     vernac_make_definition_by_tactic ~poly name ty tac
   }
   | [ "Make" "Definition" ident(name) ":" constr(ty) ":=" tactic(tac) ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_definition_by_tactic ~poly name ty tac
   }
 END

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

@@ -43,7 +43,7 @@ let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr
       EConstr.to_constr sigma (EConstr.Vars.subst_var sigma name cty)
     in
     let sigma = Evd.collapse_sort_variables sigma in
-    let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl 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 ->
       let () = Global.push_context_set ctx in

src/Rewriter/Util/plugins/rewriter_build.mli.v92

@@ -1,3 +1,3 @@
-val vernac_rewriter_emit_inductives : poly:bool -> Constrexpr.constr_expr -> Names.Id.t -> Names.Id.t -> Names.Id.t -> Names.Id.t -> unit
+val vernac_rewriter_emit_inductives : poly:PolyFlags.t -> Constrexpr.constr_expr -> Names.Id.t -> Names.Id.t -> Names.Id.t -> Names.Id.t -> unit
 
-val vernac_make_rewriter : poly:bool -> ?var_like_idents:(Constrexpr.constr_expr option) -> ?include_interp:bool -> ?skip_early_reduction:bool -> ?skip_early_reduction_no_dtree:bool -> ?extra:(Constrexpr.constr_expr option) -> Names.Id.t -> Constrexpr.constr_expr -> unit
+val vernac_make_rewriter : poly:PolyFlags.t -> ?var_like_idents:(Constrexpr.constr_expr option) -> ?include_interp:bool -> ?skip_early_reduction:bool -> ?skip_early_reduction_no_dtree:bool -> ?extra:(Constrexpr.constr_expr option) -> Names.Id.t -> Constrexpr.constr_expr -> unit

src/Rewriter/Util/plugins/rewriter_build_plugin.mlg.v92

@@ -9,74 +9,74 @@ DECLARE PLUGIN "coq-rewriter.rewriter_build"
 
 VERNAC COMMAND EXTEND RewriterEmitInductives CLASSIFIED AS SIDEFF
   | [ "Rewriter" "Emit" "Inductives" "From" "Scraped" constr(scraped_data) "As" ident(base_ind) ident(ident_ind) ident(raw_ident_ind) ident(pattern_ident_ind) ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_rewriter_emit_inductives ~poly scraped_data base_ind ident_ind raw_ident_ind pattern_ident_ind
   }
 END
 
 VERNAC COMMAND EXTEND MakeRewriter CLASSIFIED AS SIDEFF
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "delta" ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "delta" ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "inlining" constr(var_like_idents) ")" "(" "with" "extra" "idents" constr(extra) ")" "(" "with" "delta" ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~include_interp:true
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "inlining" constr(var_like_idents) ")" "(" "with" "extra" "idents" constr(extra) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "delta" ")" "(" "with" "extra" "idents" constr(extra) ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "with" "delta" ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "inlining" constr(var_like_idents) ")" "(" "with" "delta" ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
   }
   | [ "Make" ident(package) ":=" "Rewriter" "For" constr(specs_proofs) "(" "with" "extra" "idents" constr(extra) ")" "(" "with" "delta" ")" "(" "inlining" constr(var_like_idents) ")" ] -> {
-    let poly = false in
+    let poly = PolyFlags.default in
     vernac_make_rewriter ~poly package specs_proofs ~var_like_idents:(Some var_like_idents) ~include_interp:true ~extra:(Some extra)
   }
 END