Skip to content

Commit 1b16942

Browse files
committed
fix warning and remove debug prints
1 parent aecee52 commit 1b16942

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

hb.elpi

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1548,7 +1548,7 @@ export-mixin-coercion ClassName (some C) :-
15481548
coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).
15491549

15501550
pred mc-compat-structure i:string, i:modpath, i:list mixinname, i:int, i:classname, i:term, i:option gref.
1551-
mc-compat-structure ModuleName Module NewMixins CNParams ClassName ClassProjection Axioms :- std.do! [
1551+
mc-compat-structure ModuleName _Module NewMixins CNParams ClassName ClassProjection Axioms :- std.do! [
15521552
CompatModuleName is "MathCompCompat" ^ ModuleName,
15531553
coq.env.begin-module CompatModuleName none, % to avoid collisions
15541554
coq.env.begin-module ModuleName none,
@@ -2071,7 +2071,6 @@ declare-mixin-or-factory Sort1 Fields0 GRFSwP Module TheType D TheParams :- std.
20712071
if (D = asset-mixin) (Fields1 = Fields0, HackExtraPhantNo = 0)
20722072
(std.map MixinSrcClauses mixin-src_src TheHackCrap,
20732073
HackExtraPhantNo is {std.length TheHackCrap} + {std.length TheParams},
2074-
coq.say "CRAP" {std.append TheParams TheHackCrap},
20752074
hack-section-discharge-unused [TheType|{std.append TheParams TheHackCrap}] Fields0 Fields1),
20762075

20772076
if-verbose (coq.say "HB: declare record axioms_"),

0 commit comments

Comments
 (0)