The files have to be compiled with Coq version 8.7.1 Simply use: make Links from the paper "Around Classical and Intuitionistic Linear Logics": Lemma 2.1 (i) = nn.v / Lemma neg_tens_propag (ii) = nn.v / Lemma neg_plus_propag Definition 2.2 = nn.v / Fixpoint trans Lemme 2.3 = nn.v / Lemma trans_dual Proposition 2.4 = nn.v / Theorem ll_to_ill_trans Lemma 2.5 (n=0,n=2) = nn.v / Theorem ll_to_ill_trans Lemma 2.6 = ll_fragments.v / Lemma subs_llR Lemma 2.7 (=>) = ll_fragments.v / Lemma llR_to_ll (<=) = ll_fragments.v / Lemma ll_wn_wn_to_llR Lemma 2.8 (=>) = ll_fragments.v / Lemma llwnR_to_ll (<=) = ll_fragments.v / Lemma ll_wn_to_llwnR Lemma 2.9 = nn.v / Lemma back_to_llR Proposition 2.10 = nn.v / Lemma ill_trans_to_llR Lemma 2.11 (i) = nn.v / Lemma ie_dual (ii) = nn.v / Lemma ie_ie Proposition 2.12 (<=) = nn.v / Proposition llR_ie_to_ill_trans Lemma 2.13 = nn.v / Lemma ll_mix02_to_ill_trans_gen Proposition 2.14 (i) => (ii) = nn.v / Theorem ll_mix02_to_ill_trans (ii) => (iii) = nn.v / Lemma ill_trans_to_llR_one (iii) => (i) = nn.v / Theorem llR_one_to_ll_mix02 Proposition 2.16 (i) => (ii) = nn.v / Theorem ll_ll_to_ill_trans (ii) => (v) = nn.v / Theorem ill_trans_to_llR_bot (v) => (i) = nn.v / Theorem llR_bot_to_ll Lemma 2.18 = ill.v / Lemma wn_not_idefin Lemma 2.19 = ill.v / Lemma bot_not_idefin Lemma 2.20 = ill.v / Lemma wn_one_not_idefin Proposition 2.21 (i) => (ii) = nn.v / Theorem ll_mix0_to_ill_trans (ii) => (v) = nn.v / Theorem ill_trans_to_llR_wn_one (v) => (i) = nn.v / Theorem llR_wn_one_to_ll_mix0 (i) <=> (vi) = ll_fragments.v / Lemma mix0_wn_one Lemma 2.22 (included in ill.v / Lemma oc_bot_not_idefin) Lemma 2.23 = ill.v / Lemma oc_bot_not_idefin Lemma 2.24 = bbb.v / Lemma bbb_to_mix02 Proposition 2.25 = bbb.v / Lemma cut_bbb_r Proposition 2.26 (i) => (ii) = nn.v / Theorem ll_bbb_to_ill_trans (ii) => (v) = nn.v / Theorem ill_trans_to_llR_oc_bot (v) => (i) = bbb.v / Theorem bb_to_bbb Proposition 2.27 (n=2) (i) => (vi) = ll_fragments.v / Lemma mix2_to_ll (n=2) (vi) => (i) = ll_fragments.v / Lemma ll_to_mix2 (v) => (vi) = ll_fragments.v / Lemma llwnR_to_ll (vi) => (v) = ll_fragments.v / Lemma ll_wn_to_llwnR Proposition 2.28 (i) => (v) = ll_fragments.v / Lemma mix02_to_ll (v) => (i) = ll_fragments.v / Lemma ll_to_mix02 Lemma 3.2 = ill.v / Theorem ll_to_ill_oclmap_cutfree Theorem 3.3 (=>) = ill.v / Proposition ll_to_ill_oclmap_axfree Definition 3.5 = ill.v / Inductive zeropos Lemma 3.6 (Z |- 0) = ill.v / Lemma zeropos_ilr Definition 3.7 = ill.v / Inductive nonzerospos Lemma 3.8 = ill.v / Lemma dual_jfragment_zeropos Theorem 3.9 (=>) = ill.v / Theorem ll_to_ill_nzeropos_cutfree Theorem 3.11 = tl.v / Theorem ll_is_tl_axfree Lemma 4.1 = nnfoc.v / Lemma pntrans_dual Lemma 4.2 = nnfoc.v / Lemma ntrans_to_trans Theorem 4.3 = nnfoc.v / Proposition ll_to_tl Lemma 4.4 (Pi empty) = nnfoc.v / Lemma tl_to_otl Theorem 4.5 = nnfoc.v / Theorem otl_to_llfoc Corollary 4.6 = nnfoc.v / Theorem weak_focusing Lemma 5.1 (partial) = nn.v / Lemma trans_subs