Merge pull request #224 from mattam82/sort-poly-flags

Adapt to rocq-prover/rocq#21419

Author: SkySkimmer

src/wp_ffi.ml

@@ -46,7 +46,7 @@ let thaw (f: (unit, 'a) fun1): 'a tactic = f ()
 (** Comes from [coq/plugins/ltac2/tac2tactics.ml] *)
 let delayed_of_tactic (tac: 'a tactic) (env: Environ.env) (sigma: Evd.evar_map): (Evd.evar_map * 'a) =
   let _, pv = Proofview.init sigma [] in
-  let name, poly = Names.Id.of_string "ltac2_delayed", false in
+  let name, poly = Names.Id.of_string "ltac2_delayed", PolyFlags.default in
   let c, pv, _, _, _ = Proofview.apply ~name ~poly env tac pv in
   let _, sigma = Proofview.proofview pv in
   (sigma, c)

src/wp_rewrite.ml

@@ -295,7 +295,7 @@ let one_base (where: variable option) (tactic: trace tactic) (rewrite_database:
       | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) ->
         let ist = {
           Geninterp.lfun = Id.Map.empty;
-          poly = false;
+          poly = PolyFlags.default;
           extra = Geninterp.TacStore.empty
         } in Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
     in Tacticals.tclREPEAT_MAIN (tclTHEN (try_rewrite rule tac) (tclIGNORE tactic))