1 files changed, 6 insertions, 2 deletions
diff --git a/.depend.coq b/.depend.coq
index e2fa8ff5..f8b4cd6c 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -364,8 +364,12 @@ contrib/field/LegacyField_Tactic.vo: contrib/field/LegacyField_Tactic.v theories
 contrib/field/LegacyField.vo: contrib/field/LegacyField.v contrib/field/LegacyField_Compl.vo contrib/field/LegacyField_Theory.vo contrib/field/LegacyField_Tactic.vo
 contrib/fourier/Fourier_util.vo: contrib/fourier/Fourier_util.v theories/Reals/Rbase.vo
 contrib/fourier/Fourier.vo: contrib/fourier/Fourier.v contrib/ring/quote.cmo contrib/ring/ring.cmo contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo contrib/field/field.cmo contrib/fourier/Fourier_util.vo contrib/field/LegacyField.vo theories/Reals/DiscrR.vo
-contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo
-contrib/subtac/Utils.vo: contrib/subtac/Utils.v
+contrib/subtac/SubtacTactics.vo: contrib/subtac/SubtacTactics.v theories/Logic/Eqdep.vo
+contrib/subtac/Heq.vo: contrib/subtac/Heq.v theories/Logic/JMeq.vo
+contrib/subtac/Utils.vo: contrib/subtac/Utils.v contrib/subtac/SubtacTactics.vo theories/Bool/Sumbool.vo theories/Logic/ProofIrrelevance.vo contrib/subtac/Heq.vo
+contrib/subtac/FixSub.vo: contrib/subtac/FixSub.v theories/Init/Wf.vo contrib/subtac/Utils.vo theories/Arith/Wf_nat.vo theories/Arith/Lt.vo
+contrib/subtac/Subtac.vo: contrib/subtac/Subtac.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo
+contrib/subtac/FunctionalExtensionality.vo: contrib/subtac/FunctionalExtensionality.v contrib/subtac/Utils.vo contrib/subtac/FixSub.vo
 contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theories/NArith/BinPos.vo
 contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo
 contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo