1 files changed, 11 insertions, 0 deletions
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 47e69acfe0..174be06e55 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -18,3 +18,14 @@
        let t = 1 
        let u = The.External.t (* ?? *)
     end
+
+ 20. Support the .v-as-internal-module, like in 
+    
+    <file A.v>
+    Definition foo :=O.
+    <End file A.v>
+
+    <at toplevel>
+    Require A.
+    Module M:=A
+    Extraction M.
+\ No newline at end of file