diff --git a/HB/structure.elpi b/HB/structure.elpi
index 8cdfea31..0ed1a487 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -580,7 +580,13 @@ mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "Type" ; get-option ID ""
 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 :- get-option ID "off", !,
+  @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 T (w-params.cons ID Ty W) R :- not (get-option ID _), !,
+  if (coq.safe-dest-app Ty (global GR) _, is-structure GR)
+     (coq.error "HB: parameter" ID "is a structure but no form of inference specified")
+     true,
   @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,