Skip to content

Commit 07dced8

Browse files
committed
fix HB.tag
1 parent 8a89d80 commit 07dced8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

structures.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1038,7 +1038,7 @@ main [const-decl Name (some BodySkel) AritySkel] :- !, std.do! [
10381038
coq.arity->term Arity Ty,
10391039
std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "HB: body illtyped",
10401040
with-attributes (with-logging (std.do! [
1041-
log.coq.env.add-const-noimplicits Name Body Ty @transparent! C,
1041+
log.coq.env.add-const Name Body Ty @transparent! C,
10421042
coq.arity->implicits Arity CImpls,
10431043
if (coq.any-implicit? CImpls)
10441044
(@global! => coq.arguments.set-implicit (const C) [CImpls])

0 commit comments

Comments
 (0)