I am writing something heavily involving typeclasses and I would like to utilize hints to ease proving local lemmas as well as exported theorems.

For instance, consider

Class MyClass (A : Type) :=
  connect : A -> A -> Prop.

Fixpoint chain [A] [C : MyClass A] (l : list A) {struct l} : Prop :=
  match l with
  | [] | [_] => True
  | a0 :: (a1 :: _ as rest) => connect a0 a1 / chain rest
  end.

Lemma chain_seq : forall {A} `{C : MyClass A} l1 l2,
    chain l1 -> chain l2 -> chain (l1 ++ l2).
Admitted.

Lemma chain_seq_seq : forall {A} `{C : MyClass A} l1 l2 l3,
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
Admitted.

(* and so on... *)

It’s quite annoying to specify that {A} {C : MyClass A} in every single lemma or definition (imagine having more parameters and more classes). Thankfully, we have the Section construction to help:

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  Admitted.

Way better. Now I add a hint for the first theorem and use it to show the second one:

Section ChainFacts.
  Variable A : Type.
  Context `{C : MyClass A}.

  Lemma chain_seq : forall l1 l2,
      chain l1 -> chain l2 -> chain (l1 ++ l2).
  Admitted.
  Hint Resolve chain_seq.

  Lemma chain_seq_seq : forall l1 l2 l3,
      chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
    intros. auto.
  Qed.
End ChainFacts.

That works. However, it does not after I exit the section:

End ChainFacts.

#[export] Instance nat_connect : (MyClass nat) := eq.

Lemma chain_seq_seq_out : forall  [l1 l2 l3 : list nat],
    chain l1 -> chain l2 -> chain l3 -> chain (l1 ++ l2 ++ l3).
  intros. now auto.
  (* Tactic failure: Cannot solve this goal. *)

That is because hints are always section-local, which I frankly speaking do not like. I really want to be able to use hints right after each lemma definition, but I also want to export them to be used externally. Currently I see two exits from this situation:

• Not use sections (and suffer the pain of writing all class-related stuff every single time)
• Maintain a copy of all hint declarations right after closing the section. Bonus fun points: do it for each time a section is nested.

Is there anything else I can do?