I’m learning how to use the FMapInterface class of modules in Coq. A search for FMapInterface led me to A Machine Checked Model of Idempotent MGU Axioms For
Lists of Equational Constraints which had a link to its corresponding Coq script. Poking around in that script led me to the line:

Module Nat_as_MyOT <: UsualOrderedType := Nat_as_OT.

I looked up the meaning of the <: syntax. The reference manual explains that it “starts an interactive module satisfying each” subsequent module type. The ModuleSystemTutorial page also has more information on how modules are used.