From 4542b75e0efb616d181f601a4b56a11a3141392a Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 28 May 2024 13:10:24 +0200 Subject: [PATCH] fix name --- HB/structure.elpi | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HB/structure.elpi b/HB/structure.elpi index 9d3d8fd6..9d1e7477 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -112,7 +112,7 @@ declare Module BSkel Sort :- std.do! [ (if-arg-sort (private.declare-sort-coercion-elpi (global Structure) (global (const ArgSortCst))), private.declare-sort-coercion-elpi (global Structure) SortProjection), - private.declare-generic-coercion-elpi Structure, + private.declare-reverse-coercion-elpi Structure, if-verbose (coq.say {header} "exporting unification hints"), ClassAlias => Factories => GRDepsClauses => @@ -558,8 +558,8 @@ declare-sort-coercion-elpi Structure Proj :- coq.elpi.accumulate _ "coercion.db" (clause _ _ Clause). % Declares a reverse coercion for the sort projection in elpi's coercion db -pred declare-generic-coercion-elpi i:gref. -declare-generic-coercion-elpi Structure :- +pred declare-reverse-coercion-elpi i:gref. +declare-reverse-coercion-elpi Structure :- if-verbose (coq.say {header} "declare reverse coercion in elpi"),