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

Author: Lysxia

plugin/compat.ml.cppo

@@ -41,3 +41,9 @@ type indirect_accessor = unit
 type 'a with_accessor = 'a
 let apply_accessor f ~opaque_access:() = f
 #endif
+
+#if COQ_VERSION >= (9,2,0)
+let univ_poly = PolyFlags.of_univ_poly
+#else
+let univ_poly b = b
+#endif

plugin/compat.mli.cppo

@@ -14,3 +14,9 @@ type 'a with_accessor = 'a
 
 (* Compat adaptor for Coq functions *)
 val apply_accessor : 'a with_accessor -> opaque_access:indirect_accessor -> 'a
+
+#if COQ_VERSION >= (9,2,0)
+val univ_poly : bool -> PolyFlags.t
+#else
+val univ_poly : bool -> bool
+#endif

plugin/iOLib.ml

@@ -302,7 +302,7 @@ let mk_ref s = CAst.make @@ CRef (qualid_of_string s, None)
 (** [define env evd c] introduces a fresh constant name for the term [c]. *)
 let define env evd c =
   let (evd,_) = Typing.type_of env evd c in
-  let univs = Evd.univ_entry ~poly:true evd in
+  let univs = Evd.univ_entry ~poly:(Compat.univ_poly true) evd in
   let fn = fresh_name "quickchick" in
   (* TODO: Maxime - which of the new internal flags should be used here? The names aren't as clear :) *)
   let _ : Constant.t = declare_constant ~name:fn ~kind:Decls.(IsDefinition Definition)