Skip to content

Commit 22688a3

Browse files
committed
quick fix for reversible coercions
1 parent 78ba9b6 commit 22688a3

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

HB/common/log.elpi

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -361,7 +361,7 @@ coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notati
361361
coq.vernac->ppabbrterm NParams Term StrParams B.
362362
coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :-
363363
local->locality Local Locality.
364-
coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
364+
coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "#[reversible] Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
365365
coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S', S is S' ^ "." ^ {coq.gref->id SRC},
366366
if2 (TGT = sortclass) (T = "Sortclass")
367367
(TGT = funclass) (T = "Funclass")

0 commit comments

Comments
 (0)