diff --git a/doc/gf-modules.html b/doc/gf-modules.html
index 74cabe654..0a085ac49 100644
--- a/doc/gf-modules.html
+++ b/doc/gf-modules.html
@@ -660,12 +660,97 @@ is possible, as always, between modules of the same type.
Using an interface
+An interface or an instance
+can be opened in
+a concrete using the same syntax as when opening
+a resource. For an instance, the semantics
+is the same as when opening the definitions together with
+the type signatures - one can think of an interface
+and an instance of it forming an ordinary
+resource. Opening an interface, however,
+is different: functions that are only declared without
+having a definition cannot be compiled (inlined), and nor
+can functions whose definitions depend on undefined functions.
+
+
+
+A module that opens an interface is therefore
+incomplete, and has to be completed with an
+instance of the interface to become complete. To make
+this situation clear, GF requires any module that opens an
+interface to be marked as incomplete. Thus
+the module
+
+ incomplete concrete DocMarkup of Doc = open Markup in {
+ ...
+ }
+
+uses the interface Markup to place markup in
+chosen places in its linearization rules, but the
+implementation of markup - whether in HTML or in LaTeX - is
+left unspecified. This is a powerful way of sharing
+the code of a whole module.
+
+
+
+Another terminology for incomplete modules is
+parametrized modules or functors.
+The interface gives the list of parameters
+that the functor depends on.
+
Instantiating an interface
+To complete an incomplete module, each inteface
+that it opens has to be provided an instance. The following
+syntax is used for this:
+
+ concrete DocHTML of Doc = DocMarkup with (Markup = MarkupHTML) ;
+
+Instantiation of Markup with MarkupLatex is
+another one-liner.
+
+
+
+If more interfaces than one are instantiated, a comma-separated
+list of equations in parentheses is used, e.g.
+
+ concrete RulesIta = CategoriesIta ** RulesRomance with
+ (TypesRomance = TypesIta), (SyntaxRomance = SyntaxIta) ;
+
+(an example from the GF resource grammar library, where languages for
+Romance languages share two interfaces).
+All interfaces that are opened in the completed model
+must be completed.
+
+
+
+Notice that the completion of an incomplete module
+may at the same time extend modules of the same type (which need
+not be completions). But it cannot add new judgements.
+
Compiling interfaces, instances, and parametrized modules
+Interfaces, instances, and parametric modules are purely a
+front-end feature of GF: these module types do not exist in
+the gfc and gfr formats. The compiler has
+nevertheless keep track of their dependencies and modification
+times. Here is a summary of how they are compiled:
+
+- an interface is compiled into a resource with an empty body
+
- an instance is compiled into a resource in union with its
+ interface
+
- an incomplete module (concrete or resource) is compiled
+ into a module of the same type with an empty body
+
- a completion module (concrete or resource) is compiled
+ into a module of the same type by compiling its functor so that, instead of
+ each interface, its given instance is used
+
+This means that some generated code is duplicated, because those operations that
+do have complete definitions in an interface are copied to each of
+the instances
+
Transfer modules