Skip to content

Commit 084a42c

Browse files
committed
Adapt to rocq-prover/rocq#21617 (TacAlias -> TacAbbrev)
1 parent 0401985 commit 084a42c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/tac2compile.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1217,7 +1217,7 @@ let perform_compile ?(recursive=true) qidl =
12171217
in
12181218
match kn with
12191219
| TacConstant kn -> kn
1220-
| TacAlias _ ->
1220+
| TacAbbrev _ ->
12211221
CErrors.user_err ?loc:qid.CAst.loc Pp.(str "Not a definition " ++ Libnames.pr_qualid qid))
12221222
in
12231223
compile ~recursive knl

0 commit comments

Comments
 (0)