diff --git a/lib/gallinaGen.ml b/lib/gallinaGen.ml
index dffe27f..c9ddb5e 100644
--- a/lib/gallinaGen.ml
+++ b/lib/gallinaGen.ml
@@ -76,12 +76,12 @@ let fixpointBody_ name binders rtype body struc =
   let open Vernacexpr in
   let feg = { fname=lident_ name;
               univs=None;
-              rec_order=Some (CAst.make (Constrexpr.CStructRec (lident_ struc)));
               binders;
               rtype;
               body_def=Some body;
               notations=[] } in
-  feg
+  let rec_order = Some (CAst.make (Constrexpr.CStructRec (lident_ struc))) in
+  rec_order, feg
 
 
 let match_ cexpr ?rtype bexprs =
diff --git a/lib/vernacGen.ml b/lib/vernacGen.ml
index 0c6ac9d..ecab136 100644
--- a/lib/vernacGen.ml
+++ b/lib/vernacGen.ml
@@ -51,10 +51,10 @@ let fixpoint_ ~is_rec fexprs =
   | [] -> failwith "fixpoint called without fixpoint bodies"
   | fexprs_nempty ->
     if is_rec
-    then unit_of_vernacs [ VernacSynPure (VernacFixpoint (NoDischarge, fexprs)) ]
+    then unit_of_vernacs [ VernacSynPure (VernacFixpoint (NoDischarge, List.split fexprs)) ]
     (* if the fixpoint is declared non-recursive we try to turn it into a definition *)
     else match fexprs_nempty with
-      | [{ fname={ v=fname; _ }; binders; rtype; body_def=Some body; _}] ->
+      | [_, { fname={ v=fname; _ }; binders; rtype; body_def=Some body; _}] ->
         definition_ (Names.Id.to_string fname) binders ~rtype body
       | [fexpr] -> failwith "Malformed fixpoint body"
       | _ -> failwith "A non recursive fixpoint degenerates to a definition so it should only have one body"