diff --git a/.gitignore b/.gitignore
index 6d5c40f823ad0bf6a4aee0754a0c85f0bceb3251..e35984494b150fc832f1dddd373334c216bf16ca 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,6 +29,7 @@ why3.conf
 /distrib
 /why3regtests.err
 /why3regtests.out
+/META
 
 # /lib/why3/
 /lib/why3/META
@@ -100,6 +101,7 @@ why3.conf
 /doc/manual.gls
 /doc/manual.ist
 /doc/manual.out
+/doc/manual.image.out
 /doc/*.haux
 /doc/*.pdf
 /doc/html/
@@ -200,4 +202,5 @@ pvsbin/
 /src/jessie/autom4te.cache/
 /src/jessie/config.log
 /src/jessie/config.status
+/src/jessie/Makefile
 /src/jessie/ptests_local_config.ml
diff --git a/src/jessie/ACSLtoWhy3.ml b/src/jessie/ACSLtoWhy3.ml
index 8eb38e26e1aaffbb363e6123150ad46bc10583a2..70cb5dd9aa71f35a0c21ce40d6be6b106ad532ad 100644
--- a/src/jessie/ACSLtoWhy3.ml
+++ b/src/jessie/ACSLtoWhy3.ml
@@ -249,7 +249,20 @@ let add_decls_as_theory theories id decls =
 
 let rec annot ~in_axiomatic a _loc (theories,decls) =
   match a with
-    | Dtype (_, _) -> Self.not_yet_implemented "annot Dtype"
+    | Dtype (lt, loc) -> 
+      let targs = 
+        List.map (fun s -> Ty.create_tvsymbol (Ident.id_fresh s)) lt.lt_params 
+      in
+      let tdef = match lt.lt_def with
+          | None -> None
+          | Some _ -> Self.not_yet_implemented "annot Dtype non abstract"
+      in
+      let ts = 
+        Ty.create_tysymbol 
+          (Ident.id_user lt.lt_name (Loc.extract loc)) targs tdef 
+      in
+      let d = Decl.create_ty_decl ts in
+      (theories,d::decls)
     | Dfun_or_pred (_, _) -> Self.not_yet_implemented "annot Dfun_or_pred"
     | Dlemma(name,is_axiom,labels,vars,p,loc) ->
       begin
diff --git a/src/jessie/tests/basic/axiomatic.c b/src/jessie/tests/basic/axiomatic.c
index 408573fab075c5d58e0506f3047af2383973a193..29c1b07719213793bb3e187e4b3d0c43eede4b89 100644
--- a/src/jessie/tests/basic/axiomatic.c
+++ b/src/jessie/tests/basic/axiomatic.c
@@ -5,9 +5,9 @@
 
 /*@ axiomatic Bag {
   @   type bag;
-  @   logic bag my_union(bag b1,bag b2);
-  @   axiom union_comm: \forall bag b1,b2;
-  @      my_union(b1,b2) == my_union(b2,b1);
+  @ //  logic bag my_union(bag b1,bag b2);
+  @ //  axiom union_comm: \forall bag b1,b2;
+  @ //     my_union(b1,b2) == my_union(b2,b1);
   @ }
   @*/
 
diff --git a/src/jessie/tests/basic/oracle/axiomatic.res.oracle b/src/jessie/tests/basic/oracle/axiomatic.res.oracle
index 2e44a819fd90353d4028e6d42121c5d85cadc5a9..85d27bb8f9f01b18b01567060426cdedc7c69acf 100644
--- a/src/jessie/tests/basic/oracle/axiomatic.res.oracle
+++ b/src/jessie/tests/basic/oracle/axiomatic.res.oracle
@@ -1,4 +1,6 @@
 [kernel] preprocessing with "gcc -C -E -I.  tests/basic/axiomatic.c"
-[kernel] Plug-in jessie3 aborted: unimplemented feature.
-         You may send a feature request at http://bts.frama-c.com with:
-         '[Plug-in jessie3] annot Dtype'.
+[jessie3] user error: WARNING: Variable Frama_C_copy_block not translated
+[jessie3] user error: WARNING: Variable Frama_C_bzero not translated
+[jessie3] found 0 decls
+[jessie3] made 1 theories
+[jessie3] running theory 1