Merge pull request #654 from LPCIC/fixup-652

fix PR #652
LPCIC · Jul 5, 2024 · 50b305a · 50b305a
2 parents 81c6c15 + 81236db
commit 50b305a
Showing 1 changed file with 8 additions and 0 deletions.
diff --git 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