fix name

math-comp · May 28, 2024 · 4542b75 · 4542b75
1 parent e375fb0
commit 4542b75
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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"),