Skip to content

Commit 78ba9b6

Browse files
committed
fix param printing
1 parent 9c3d854 commit 78ba9b6

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

HB/common/log.elpi

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -446,8 +446,8 @@ coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :-
446446
pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp.
447447
coq.vernac->ppinductiveparams [] [].
448448
coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :-
449-
PP = [box (hov 2) [str A,str ID,str " : ", TY,str B]|PPRest],
450-
decl T Name Ty, coq.name->id Name ID, coq.term->pp Ty TY,
449+
PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest],
450+
coq.term->pp T ID, decl T _ Ty, coq.term->pp Ty TY,
451451
if2 (Imp = explicit) (A = "(", B = ")")
452452
(Imp = maximal) (A = "{", B = "}")
453453
(A = "[", B = "]"),

0 commit comments

Comments
 (0)