Apply suggestions from code review

Author: CohenCyril

HB/structure.elpi

@@ -107,9 +107,8 @@ declare Module B :- std.do! [
 
   if-verbose (coq.say "HB: declaring on abbreviation"),
 
-  (pi t1 t2\ coq.notation.abbreviation ClassForAbbrev [t1, t2] (ClassForAbbrevDiag t1 t2)),
   @global! => log.coq.notation.add-abbreviation "on" 1
-    {{fun T => lp:{{ ClassForAbbrevDiag {{ T }} _ }} }} tt _,
+    {{fun T => lp:{{ ClassForAbbrev {{ T }} _ }} }} tt _,
 
   log.coq.env.end-module-name Module ModulePath,