Fix mutable skipping in recursive mode (#15)

src/tac2compile.ml

@@ -1004,7 +1004,8 @@ let rec get_dependencies ((visited, skipped_mut, knl) as acc) kn =
         kndeps
         (KNset.add kn visited, skipped_mut, knl)
     in
-    (visited, skipped_mut, kn :: knl)
+    let knl = if data.gdata_mutable then knl else kn :: knl in
+    (visited, skipped_mut, knl)
 
 let warn_skipped_mut = CWarnings.create ~name:"tac2compile-skipped-mutable" ~category:CWarnings.CoreCategories.ltac2
     (fun skipped_mut ->
@@ -1121,6 +1122,7 @@ let compile ~recursive knl =
     if recursive then get_recursive_kns knl
     else knl
   in
+  debug Pp.(fun () -> str "Compiling constants " ++ prlist_with_sep spc (Tac2print.pr_tacref Id.Set.empty) knl);
   let file, ch, prefix = get_ml_filename () in
   let kns, exts, pp = pp_code recursive prefix knl in
   let fch = Format.formatter_of_out_channel ch in

tests/_CoqProject

@@ -8,3 +8,4 @@ bug_10107.v
 minibench.v
 compiler_bug_4.v
 compiler_bug_6.v
+compiler_bug_14.v

tests/compiler_bug_14.v

@@ -0,0 +1,11 @@
+From Ltac2 Require Import Ltac2.
+Ltac2 mutable mut : unit := ().
+Ltac2 test () := match mut with () => () end.
+
+From Ltac2Compiler Require Import Ltac2Compiler.
+
+Ltac2 Compile test.
+(*
+Dynlink error: execution of module initializers in the shared library failed:
+File "plugins/ltac2/tac2env.ml", line 79, characters 2-8: Assertion failed
+*)