diff --git a/Changelog.md b/Changelog.md
index 246a3c99..1c12d44a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -4,6 +4,8 @@
 
 - **Removed** the `#[primitive_class]` attribute, making it the default.
 - **New** `HB.saturate` to saturate instances w.r.t. the current hierarchy
+- **Removed** the `#[infer]` attribute made obsolete by reverse coercions
+  since Coq 8.16
 
 ## [1.6.0] - 2023-09-20
 
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index fa7552b0..b205154b 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -29,7 +29,6 @@ with-attributes P :-
     att "mathcomp.axiom" string,
     att "short.type" string,
     att "short.pack" string,
-    att "infer" attmap,
     att "key" string,
     att "arg_sort" bool,
     att "log" bool,
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 89bf3313..1c715656 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -56,8 +56,6 @@ declare Module BSkel Sort :- std.do! [
   if-verbose (coq.say {header} "structure: mixin first class" MixinFirstClass),
 
 
-  private.declare-auto-infer-params-abbrev Structure MLwP LocType PHClauses,
-
   if-verbose (coq.say {header} "declaring clone abbreviation"),
   w-params.then MLwP phant.fun-real phant.fun-real
     (private.clone-phant-body ClassName SortProjection Structure) PhClone,
@@ -89,11 +87,7 @@ declare Module BSkel Sort :- std.do! [
   
   if (get-option "short.type" ShortType) (
     if-verbose (coq.say {header} "short name for type:" ShortType),
-    if (LocType = loc-abbreviation StrTypeAbbrev) (std.do! [
-      coq.notation.abbreviation-body StrTypeAbbrev NStrTypeAbbrev StrTypeTm,
-      @global! => log.coq.notation.add-abbreviation
-        ShortType NStrTypeAbbrev StrTypeTm ff _
-    ]) (@global! => log.coq.notation.add-abbreviation
+    (@global! => log.coq.notation.add-abbreviation
       ShortType 0 (global Structure) ff _)) true,
 
   coq.mk-app (global Structure) {coq.mk-n-holes {w-params.nparams MLwP}} HB_Instance,
@@ -133,7 +127,7 @@ declare Module BSkel Sort :- std.do! [
   std.flatten [
       Factories, [ClassAlias], [is-structure Structure],
       NewJoins, [class-def CurrentClass], GRDepsClauses,
-      [gref-deps GRPack MLwP], MixinMems, [StructKeyClause], PHClauses
+      [gref-deps GRPack MLwP], MixinMems, [StructKeyClause]
     ]
     NewClauses,
   acc-clauses current NewClauses,
@@ -449,9 +443,7 @@ synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :-
 
 pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl.
 pred mk-record+sort-field i:universe, i:name, i:term, i:(term -> record-decl), o:indt-decl.
-mk-record+sort-field Sort _ T F (record RecordName (sort Sort) "Pack" (field _ "sort" T F)) :- !, std.do! [
-  if (get-option "infer" _) (RecordName = "type_") (RecordName = "type")
-].
+mk-record+sort-field Sort _ T F (record "type" (sort Sort) "Pack" (field _ "sort" T F)).
 
 pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
 mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global ClassName|Args]) _\end-record) :-
@@ -591,27 +583,6 @@ pack-body.aux PL T BuildC PackS  Body :- !, std.do! [
   mk-app (global PackS) {std.append PL [T, Class]} Body
 ].
 
-pred declare-auto-infer-params-abbrev i:structure, i:mixins, o:located, o:list prop.
-declare-auto-infer-params-abbrev GR MLwP (loc-abbreviation Abbrev) [phant-abbrev GR (const PhC) Abbrev] :-
-  get-option "infer" Map, !,
-  Map => mk-infer (global GR) MLwP PhT,
-  phant.add-abbreviation "type" PhT PhC Abbrev.
-declare-auto-infer-params-abbrev GR _ (loc-gref GR) [].
-
-pred mk-infer i:term, i:mixins, o:phant-term.
-mk-infer T (w-params.nil _ _ _) PH :- phant.init T PH.
-mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "Type" ; get-option ID ""), !,
-  @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
-  phant.fun-infer-type sortclass {coq.id->name ID} Ty PhT R.
-mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "_ -> _"), !,
-  @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
-  phant.fun-infer-type funclass {coq.id->name ID} Ty PhT R.
-mk-infer T (w-params.cons ID Ty W) R :- not (get-option ID _), !,
-  @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
-  phant.fun-real {coq.id->name ID} Ty PhT R.
-mk-infer _ (w-params.cons ID _ _) _ :- get-option ID Infer,
-  coq.error "Automatic inference of paramter" ID "from" Infer "not supported".
-
 pred mk-infer-key i:class, i:term, i:mixins, i:term, o:phant-term.
 mk-infer-key CoeClass K (w-params.nil ID _ _) St PhK :-
   @pi-parameter ID St t\ phant.init {mk-app K [t]} (PhKBo t),
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index 391e6c39..7a243c1b 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -60,7 +60,6 @@ tests/duplicate_structure.v
 tests/instance_params_no_type.v
 tests/test_CS_db_filtering.v
 tests/subtype.v
-tests/infer.v
 tests/exports.v
 tests/exports2.v
 tests/log_impargs_record.v
diff --git a/structures.v b/structures.v
index fb904876..9326c4fc 100644
--- a/structures.v
+++ b/structures.v
@@ -581,14 +581,6 @@ HB.structure Definition StructureName params :=
   Supported attributes:
   - [#[mathcomp]] attempts to generate a backward compatibility layer with mathcomp:
     trying to infer the right [StructureName.pack],
-  - [#[infer(variable)]], where [variable : pT] belongs to [params] and is a structure
-    (e.g. from the hierarchy) with a coercion/canonical projection [pT >-> Sortclass].
-    It modifies the notation [StructureName.type] so as to accept [variable : Type] instead,
-    and will try to infer its [pT] by unification (using canonical structure inference),
-    This is essential in [Lmodule.type R] where [R] should have type [Ring.type]
-    but any [Type] which is canonically a [Ring.type] is accepted thanks to [#[infer(R)]].
-    If the carrier of the structure [S] is not a [Type] but rather a function, one has
-    to write [#[infer(S = "_ -> _")]].
   - [#[arg_sort]] defines an alias [StructureName.arg_sort] for [StructureName.sort],
     and declares it as the main coercion. [StructureName.sort] is still declared as a coercion
     but the only reason is to make sure Coq does not print it.
diff --git a/tests/funclass.v b/tests/funclass.v
index 29d278f1..55c5c72d 100644
--- a/tests/funclass.v
+++ b/tests/funclass.v
@@ -50,7 +50,6 @@ HB.instance Definition x5 :=
 Check Monoid.on mult.
 
 HB.mixin Record silly (T1 : Type) (F : Monoid.type T1) (T : Type) := { xx : T }.
-#[infer(F = "_ -> _")]
 HB.structure Definition wp T (F : Monoid.type T) := { A of silly T F A }.
 
 #[skip="8.11"]
diff --git a/tests/infer.v b/tests/infer.v
deleted file mode 100644
index 450d5a21..00000000
--- a/tests/infer.v
+++ /dev/null
@@ -1,29 +0,0 @@
-From HB Require Import structures.
-
-HB.mixin Record foom T := {
-  op : T -> T -> T
-}.
-
-HB.structure Definition foo := { T of foom T }.
-
-HB.instance Definition i := foom.Build nat plus.
-
-#[key="T"]
-HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := {
-  law : P -> T -> A -> B
-}.
-
-#[infer(P)]
-HB.structure Definition bar A P B := { T of barm A P B T }.
-
-HB.check (bar.type_ bool nat bool).
-Print bar.phant_type.
-Print bar.type.
-Check bar.type bool nat bool.
-
-Fail #[infer(P = "whatever")]
-HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }.
-
-#[infer(P = "Type")]
-HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }.
-Check bar1.type nat.