diff --git a/src/tac2compile.ml b/src/tac2compile.ml index f680cac..0321695 100644 --- a/src/tac2compile.ml +++ b/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 -> diff --git a/tests/_CoqProject b/tests/_CoqProject index 0fca7c6..c0c2606 100644 --- a/tests/_CoqProject +++ b/tests/_CoqProject @@ -8,3 +8,4 @@ bug_10107.v minibench.v compiler_bug_4.v compiler_bug_6.v +compiler_bug_14.v diff --git a/tests/compiler_bug_14.v b/tests/compiler_bug_14.v new file mode 100644 index 0000000..edfe167 --- /dev/null +++ b/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 +*)