1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
new file mode 100644
index 00000000..6d8ce7c5
--- /dev/null
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -0,0 +1,22 @@
+open Names
+
+let evil t f =
+  let open Univ in
+  let open Entries in
+  let open Decl_kinds in
+  let open Constr in
+  let k = IsDefinition Definition in
+  let u = Level.var 0 in
+  let tu = mkType (Universe.make u) in
+  let te = Declare.definition_entry
+      ~univs:(Monomorphic_const_entry (ContextSet.singleton u)) tu
+  in
+  let tc = Declare.declare_constant t (DefinitionEntry te, k) in
+  let tc = mkConst tc in
+
+  let fe = Declare.definition_entry
+      ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~types:(Term.mkArrow tc tu)
+      (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
+  in
+  ignore (Declare.declare_constant f (DefinitionEntry fe, k))