Skip to content

Commit c5de016

Browse files
committed
Fix build on master (parallel merges of erelevance and ltac2 API)
1 parent 4352c71 commit c5de016

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)