Merge pull request #19 from SkySkimmer/erelevance

Adapt to coq/coq#18938 (EConstr.ERelevance)
SkySkimmer · Apr 23, 2024 · ce8ed08 · ce8ed08
2 parents cd19535 + 05f79a3
commit ce8ed08
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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 *)