remove dead code

math-comp · Feb 25, 2021 · a83d384 · a83d384
1 parent 4c7f7d9
commit a83d384
Showing 1 changed file with 0 additions and 13 deletions.
diff --git a/hb.elpi b/hb.elpi
@@ -1785,19 +1785,6 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [
   GRDepsClauses => declare-factory-abbrev Module FactAbbrev,
 ].
 
-pred hack-append-phant-unify i:int, i:phant-term, o:phant-term.
-hack-append-phant-unify 0 X Y :- append-phant-unify X Y.
-hack-append-phant-unify M X Y :- M > 0, !,
-  N is M - 1,
-  hack-append-phant-unify N {append-phant-unify X} Y.
-
-
-pred hack-section-discharge-unused i:list term, i:record-decl, o:record-decl.
-hack-section-discharge-unused [] F F.
-hack-section-discharge-unused [T|TS] F (field _ "_" {{ lib:hb.unify lp:TT lp:TT lp:T lp:T lib:hb.nomsg }} _\ F0) :-
-  std.assert-ok! (coq.typecheck T TT) "wtf",
-  hack-section-discharge-unused TS F F0.
-
 pred abstract-indt-decl i:list term, i:indt-decl, o:indt-decl.
 abstract-indt-decl [] X X1 :- copy-indt-decl X X1.
 abstract-indt-decl [global (const C)|CS] X (parameter ID explicit Ty1 X1) :-