Skip to content

Commit 03d371d

Browse files
Merge PR #18974: Fix build on master (parallel merges of erelevance and ltac2 API)
Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
2 parents 4352c71 + c5de016 commit 03d371d

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

plugins/ltac2/tac2core.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -831,7 +831,8 @@ let () =
831831
define "constr_binder_type" (repr_ext val_binder @-> ret constr) @@ fun (_, ty) -> ty
832832

833833
let () =
834-
define "constr_binder_relevance" (repr_ext val_binder @-> ret relevance) @@ fun (na, _) -> na.binder_relevance
834+
define "constr_binder_relevance" (repr_ext val_binder @-> ret relevance) @@ fun (na, _) ->
835+
EConstr.Unsafe.to_relevance na.binder_relevance
835836

836837
let () =
837838
define "constr_has_evar" (constr @-> tac bool) @@ fun c ->

0 commit comments

Comments
 (0)