From 05f79a3ca0012b32f452138245f7dd15365a5c72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Apr 2024 13:49:16 +0200 Subject: [PATCH] Adapt to coq/coq#18938 (EConstr.ERelevance) --- src/lean.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/lean.ml b/src/lean.ml index 9b63edd..4d04668 100644 --- a/src/lean.ml +++ b/src/lean.ml @@ -655,6 +655,7 @@ let to_annot rels n t uconv = let env = Environ.set_universes uconv.graph env in let evd = Evd.from_env env in let r = Retyping.relevance_of_type env evd (EConstr.of_constr t) in + let r = EConstr.Unsafe.to_relevance r in Context.make_annot (N.to_name n) r (* bit n of [int_of_univs univs] is 1 iff [List.nth univs n] is SProp *)