Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

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))