From 81236db997f6357dc78fb702efbb718127fb0584 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 5 Jul 2024 14:48:02 +0200
Subject: [PATCH] fix PR #652

---
 src/coq_elpi_builtins.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 667affb02..e4e83e08f 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -518,12 +518,20 @@ let set_accumulate_to_db_interp, get_accumulate_to_db_interp =
   (fun x -> f := x),
   (fun () -> !f)
 
+[%%if coq = "8.19" || coq = "8.20"]
 let is_global_level env u =
   try
     let set = Univ.Level.Set.singleton u in
     let () = UGraph.check_declared_universes (Environ.universes env) set in
     true
   with UGraph.UndeclaredLevel _ -> false
+[%%else]
+let is_global_level env u =
+  let set = Univ.Level.Set.singleton u in
+  match UGraph.check_declared_universes (Environ.universes env) set with
+  | Ok () -> true
+  | Error _ -> false
+[%%endif]
 
 let err_if_contains_alg_univ ~depth t =
   let global_univs = UGraph.domain (Environ.universes (Global.env ())) in