Coq Section: require typeclass instance

Question

Require Import Relations RelationClasses.

Section MySection.
  Variable A : Type.
  Variable R : relation A.
  (* ... *)
End MySection.

How could I require R to be a partial order?

Answer 1

There is the Context syntax, see The Coq Reference manual, §20.4:

To ease the parametrization of developments by type classes, we provide a new way to introduce variables into section contexts, compatible with the implicit argument mechanism. The new command works similarly to the Variables vernacular (see 1.3.1), except it accepts any binding context as argument.

Example:

From Coq Require Import RelationClasses.

Generalizable Variable A eqA R.

Section MySection.
  Context `{PO : PartialOrder A eqA R}.
  (* ... *)
End MySection.