diff --git a/HB/howto.elpi b/HB/howto.elpi
index da46e4fbc..7d6b6a23c 100644
--- a/HB/howto.elpi
+++ b/HB/howto.elpi
@@ -148,7 +148,9 @@ pp-solutions LLF :-
     str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):",
     {about.bulletize SLLF pp-solution}],
   % print
-  coq.say {coq.pp->string PpSolutions},  
+  coq.say {coq.pp->string PpSolutions},
+  coq.say,
+  coq.say "For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances",
   coq.say.
 
 pred pp-solution i:list factoryname, o:coq.pp.
diff --git a/tests/howto.v.out b/tests/howto.v.out
index a83cbce85..9afb95c2f 100644
--- a/tests/howto.v.out
+++ b/tests/howto.v.out
@@ -9,6 +9,8 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
     - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_TYPE
     - AddAG_of_TYPE; BiNearRing_of_AddMonoid
@@ -16,6 +18,8 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddAG_of_TYPE; SemiRing_of_AddComoid
     - AddComoid_of_TYPE; Ring_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_TYPE
     - AddAG_of_TYPE; BiNearRing_of_AddMonoid
@@ -27,6 +31,8 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
     - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - Ring_of_TYPE
     - AddAG_of_TYPE; BiNearRing_of_AddMonoid
@@ -34,6 +40,8 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddAG_of_TYPE; SemiRing_of_AddComoid
     - AddComoid_of_TYPE; Ring_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 The command has indeed failed with message:
 HB: no solution found, try to increase search depth.
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
@@ -42,14 +50,20 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddAG_of_AddComoid; Ring_of_AddAG
     - AddAG_of_AddComoid; SemiRing_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - BiNearRing_of_AddMonoid
     - Ring_of_AddAG
     - SemiRing_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - BiNearRing_of_AddMonoid
     - Ring_of_AddAG
     - SemiRing_of_AddComoid
 
+For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances
+
 HB: nothing to do.