some examples documented for the gallery

examples/all_distinct.mlw

 
 (** Check an array of integers for duplicate values,
-    using the fact that values are in interval [0,m-1]. *)
+    using the fact that values are in interval [0,m-1].
+
+    Authors: Jean-Christophe Filliâtre (CNRS)
+             Martin Clochard (École Normale Supérieure)
+*)
 
 module AllDistinct
 

examples/coincidence_count.mlw

@@ -7,6 +7,9 @@
     order and without duplicate elements, and you count the number of
     elements that appear in both sequences (in linear time and constant
     space).
+
+    Authors: Jean-Christophe Filliâtre (CNRS)
+             Andrei Paskevich (Université Paris Sud)
 *)
 
 module CoincidenceCount

examples/linear_probing.mlw

 
 (** Hash tables using linear probing
 
-    Authors: Martin Clochard (École Normale Supérieure)
-             Jean-Christophe Filliâtre (CNRS)
+    Authors: Jean-Christophe Filliâtre (CNRS)
+             Martin Clochard (École Normale Supérieure)
 *)
 
 module HashedTypeWithDummy

examples/skew_heaps.mlw

 
+(** Skew heaps
+
+    Author: Jean-Christophe Filliâtre (CNRS)
+*)
+
 module Heap
 
   use import int.Int

examples/topological_sorting.mlw

+
+(** Topological sorting
+
+    Author: François Bobot (CEA)
+*)
+
 theory Graph
 
   use export int.Int