]> matita.cs.unibo.it Git - helm.git/commitdiff
Added boolean "is_inductive" to NReference.Ind
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 13 May 2008 09:40:21 +0000 (09:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 13 May 2008 09:40:21 +0000 (09:40 +0000)
helm/software/components/ng_kernel/.depend.opt
helm/software/components/ng_kernel/alluris.txt
helm/software/components/ng_kernel/nCic2OCic.ml
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicPp.ml
helm/software/components/ng_kernel/nCicTypeChecker.ml
helm/software/components/ng_kernel/nReference.ml
helm/software/components/ng_kernel/nReference.mli
helm/software/components/ng_kernel/oCic2NCic.ml

index 0900c08de7b9edaf24d4a4c8cbf36b789f39944a..8396f2c58661fdd85b7349bd4828ffc2db3dd5f3 100644 (file)
@@ -2,6 +2,7 @@ nReference.cmi: nUri.cmi
 nCicUtils.cmi: nCic.cmx 
 nCicSubstitution.cmi: nCic.cmx 
 oCic2NCic.cmi: nCic.cmx 
+nCicLibrary.cmi: nUri.cmi nCic.cmx 
 nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx 
 nCicPp.cmi: nCic.cmx 
 nCicReduction.cmi: nCic.cmx 
@@ -21,12 +22,14 @@ oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmx \
     oCic2NCic.cmi 
 oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \
     oCic2NCic.cmi 
-nCicEnvironment.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCic.cmx \
+nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCicLibrary.cmi 
+nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCicLibrary.cmi 
+nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx \
     nCicEnvironment.cmi 
-nCicEnvironment.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCic.cmx \
+nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \
     nCicEnvironment.cmi 
-nCicPp.cmo: nUri.cmi nReference.cmi nCicEnvironment.cmi nCic.cmx nCicPp.cmi 
-nCicPp.cmx: nUri.cmx nReference.cmx nCicEnvironment.cmx nCic.cmx nCicPp.cmi 
+nCicPp.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx nCicPp.cmi 
+nCicPp.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx nCicPp.cmi 
 nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
     nCicEnvironment.cmi nCic.cmx nCicReduction.cmi 
 nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
index 10afda9d9c2abc8d92d9016c828c34eadc889712..45c8be73436533df831e9639b8ef62e686155053 100644 (file)
-cic:/matita/tests/absurd/stupid.con
-cic:/matita/tests/apply2/test.con
-cic:/matita/tests/apply/a.con
-cic:/matita/tests/apply/b.con
-cic:/matita/tests/apply/c.con
-cic:/matita/tests/apply/d.con
-cic:/matita/tests/applys/foo.con
-cic:/matita/tests/applys/prova2.con
-cic:/matita/tests/applys/prova.con
-cic:/matita/tests/assumption/stupid.con
-cic:/matita/tests/bad_induction/absurd.con
-cic:/matita/tests/bad_induction/bad_ind.con
-cic:/matita/tests/bool/bool507.con
-cic:/matita/tests/change/stupid.con
-cic:/matita/tests/change/t.con
-cic:/matita/tests/clearbody/stupid.con
-cic:/matita/tests/clear/stupid.con
-cic:/matita/tests/coercions/a.con
-cic:/matita/tests/coercions/c1.con
-cic:/matita/tests/coercions/c2.con
-cic:/matita/tests/coercions/c3.con
-cic:/matita/tests/coercions/c4.con
-cic:/matita/tests/coercions/church.con
-cic:/matita/tests/coercions_contravariant/A1.con
-cic:/matita/tests/coercions_contravariant/A.con
-cic:/matita/tests/coercions_contravariant/B1.con
-cic:/matita/tests/coercions_contravariant/B.con
-cic:/matita/tests/coercions_contravariant/c.con
-cic:/matita/tests/coercions_contravariant/d.con
-cic:/matita/tests/coercions_contravariant/f.con
-cic:/matita/tests/coercions_contravariant/foo1_1.con
-cic:/matita/tests/coercions_contravariant/foo2.con
-cic:/matita/tests/coercions_contravariant/foo3.con
-cic:/matita/tests/coercions_contravariant/foo4.con
-cic:/matita/tests/coercions_contravariant/foo.con
-cic:/matita/tests/coercions_contravariant/g.con
-cic:/matita/tests/coercions_contravariant/h.con
-cic:/matita/tests/coercions_dependent/c.con
-cic:/matita/tests/coercions_dependent/vec.ind
-cic:/matita/tests/coercions_dependent/vec_ind.con
-cic:/matita/tests/coercions_dependent/vec_inv.con
-cic:/matita/tests/coercions_dependent/veclen.con
-cic:/matita/tests/coercions_dependent/vec_rec.con
-cic:/matita/tests/coercions_dependent/vec_rect.con
-cic:/matita/tests/coercions_dependent/xxx.con
-cic:/matita/tests/coercions/double1.con
-cic:/matita/tests/coercions/double2.con
-cic:/matita/tests/coercions/double.con
-cic:/matita/tests/coercions/empty.ind
-cic:/matita/tests/coercions/empty_ind.con
-cic:/matita/tests/coercions/empty_rec.con
-cic:/matita/tests/coercions/empty_rect.con
-cic:/matita/tests/coercions/f.con
-cic:/matita/tests/coercions/foo01.con
-cic:/matita/tests/coercions/foo0.con
-cic:/matita/tests/coercions/foo.con
-cic:/matita/tests/coercions/fst.con
-cic:/matita/tests/coercions/i2pos.con
-cic:/matita/tests/coercions/if.con
-cic:/matita/tests/coercions/initial.ind
-cic:/matita/tests/coercions/initial_ind.con
-cic:/matita/tests/coercions/initial_rec.con
-cic:/matita/tests/coercions/initial_rect.con
-cic:/matita/tests/coercions/int.ind
-cic:/matita/tests/coercions/int_ind.con
-cic:/matita/tests/coercions/int_OF_initial.con
-cic:/matita/tests/coercions/int_OF_pos.con
-cic:/matita/tests/coercions/int_rec.con
-cic:/matita/tests/coercions/int_rect.con
-cic:/matita/tests/coercions/ith.con
-cic:/matita/tests/coercions/listn2function.con
-cic:/matita/tests/coercions/listn.ind
-cic:/matita/tests/coercions/listn_ind.con
-cic:/matita/tests/coercions/listn_inv.con
-cic:/matita/tests/coercions/listn_rec.con
-cic:/matita/tests/coercions/listn_rect.con
-cic:/matita/tests/coercions/map.con
-cic:/matita/tests/coercions/mapmult.con
-cic:/matita/tests/coercions/nat2int.con
-cic:/matita/tests/coercions/natlist2map.con
-cic:/matita/tests/coercions/nat_OF_initial.con
-cic:/matita/tests/coercions_nonuniform/A.con
-cic:/matita/tests/coercions_nonuniform/B.con
-cic:/matita/tests/coercions_nonuniform/B_OF_A.con
-cic:/matita/tests/coercions_nonuniform/c1.con
-cic:/matita/tests/coercions_nonuniform/c2.con
-cic:/matita/tests/coercions_nonuniform/C.con
-cic:/matita/tests/coercions_nonuniform/C_OF_A.con
-cic:/matita/tests/coercions_nonuniform/C_OF_B.con
-cic:/matita/tests/coercions_nonuniform/f1.con
-cic:/matita/tests/coercions_nonuniform/f.con
-cic:/matita/tests/coercions_nonuniform/g.con
-cic:/matita/tests/coercions_nonuniform/k.con
-cic:/matita/tests/coercions_nonuniform/test.con
-cic:/matita/tests/coercions_open/AB.con
-cic:/matita/tests/coercions_open/A.con
-cic:/matita/tests/coercions_open/A_OF_A.con
-cic:/matita/tests/coercions_open/B.con
-cic:/matita/tests/coercions_open/B_OF_A.con
-cic:/matita/tests/coercions_open/B_OF_B.con
-cic:/matita/tests/coercions_open/daemon.con
-cic:/matita/tests/coercions_open/eatA.con
-cic:/matita/tests/coercions_open/eatB.con
-cic:/matita/tests/coercions_open/jmcAB.con
-cic:/matita/tests/coercions_open/jmcBA.con
-cic:/matita/tests/coercions_open/xx.con
-cic:/matita/tests/coercions/pos2nat.con
-cic:/matita/tests/coercions/pos2nat'.con
-cic:/matita/tests/coercions/pos.ind
-cic:/matita/tests/coercions/pos_ind.con
-cic:/matita/tests/coercions/pos_rec.con
-cic:/matita/tests/coercions/pos_rect.con
-cic:/matita/tests/coercions_propagation/eject.con
-cic:/matita/tests/coercions_propagation/ejectN.con
-cic:/matita/tests/coercions_propagation/f1.con
-cic:/matita/tests/coercions_propagation/f.con
-cic:/matita/tests/coercions_propagation/F.con
-cic:/matita/tests/coercions_propagation/inject.con
-cic:/matita/tests/coercions_propagation/injectN.con
-cic:/matita/tests/coercions_propagation/NN.ind
-cic:/matita/tests/coercions_propagation/NN_ind.con
-cic:/matita/tests/coercions_propagation/NN_inv.con
-cic:/matita/tests/coercions_propagation/NN_OF_NN.con
-cic:/matita/tests/coercions_propagation/NN_rec.con
-cic:/matita/tests/coercions_propagation/NN_rect.con
-cic:/matita/tests/coercions_propagation/PN.con
-cic:/matita/tests/coercions_propagation/sigma.ind
-cic:/matita/tests/coercions_propagation/sigma_ind.con
-cic:/matita/tests/coercions_propagation/sigma_OF_NN.con
-cic:/matita/tests/coercions_propagation/sigma_OF_sigma1.con
-cic:/matita/tests/coercions_propagation/sigma_OF_sigma.con
-cic:/matita/tests/coercions_propagation/sigma_rec.con
-cic:/matita/tests/coercions_propagation/sigma_rect.con
-cic:/matita/tests/coercions_propagation/test2.con
-cic:/matita/tests/coercions_propagation/test3.con
-cic:/matita/tests/coercions_propagation/test4.con
-cic:/matita/tests/coercions_propagation/test51_byhand.con
-cic:/matita/tests/coercions_propagation/test51.con
-cic:/matita/tests/coercions_propagation/test522.con
-cic:/matita/tests/coercions_propagation/test5.con
-cic:/matita/tests/coercions_propagation/test.con
-cic:/matita/tests/coercions_russell/bind.con
-cic:/matita/tests/coercions_russell/eject.con
-cic:/matita/tests/coercions_russell/eject_opt.con
-cic:/matita/tests/coercions_russell/f.con
-cic:/matita/tests/coercions_russell/find_spec.con
-cic:/matita/tests/coercions_russell/hd.con
-cic:/matita/tests/coercions_russell/inject.con
-cic:/matita/tests/coercions_russell/inject_opt.con
-cic:/matita/tests/coercions_russell/list_OF_list.con
-cic:/matita/tests/coercions_russell/mem_x_to_ex_l1_l2.con
-cic:/matita/tests/coercions_russell/nat_return.con
-cic:/matita/tests/coercions_russell/option_OF_nat.con
-cic:/matita/tests/coercions_russell/option_OF_option.con
-cic:/matita/tests/coercions_russell/raise_exn.con
-cic:/matita/tests/coercions_russell/sigma_find_spec.con
-cic:/matita/tests/coercions_russell/sigma.ind
-cic:/matita/tests/coercions_russell/sigma_ind.con
-cic:/matita/tests/coercions_russell/sigma_OF_list.con
-cic:/matita/tests/coercions_russell/sigma_OF_nat1.con
-cic:/matita/tests/coercions_russell/sigma_OF_nat.con
-cic:/matita/tests/coercions_russell/sigma_OF_option.con
-cic:/matita/tests/coercions_russell/sigma_OF_sigma1.con
-cic:/matita/tests/coercions_russell/sigma_OF_sigma.con
-cic:/matita/tests/coercions_russell/sigma_rec.con
-cic:/matita/tests/coercions_russell/sigma_rect.con
-cic:/matita/tests/coercions_russell/tl2.con
-cic:/matita/tests/coercions_russell/tl.con
-cic:/matita/tests/coercions_russell/try_with.con
-cic:/matita/tests/coercions/T0.con
-cic:/matita/tests/coercions/T1.con
-cic:/matita/tests/coercions/T1_OF_T0.con
-cic:/matita/tests/coercions/T2.con
-cic:/matita/tests/coercions/T2_OF_T0.con
-cic:/matita/tests/coercions/T3.con
-cic:/matita/tests/coercions/T3_OF_T01.con
-cic:/matita/tests/coercions/T3_OF_T0.con
-cic:/matita/tests/coercions/T3_OF_T1.con
-cic:/matita/tests/coercions/T3_OF_T2.con
-cic:/matita/tests/comments/a.con
-cic:/matita/tests/compose/an_1.con
-cic:/matita/tests/constructor/stupid.con
-cic:/matita/tests/continuationals/branch.con
-cic:/matita/tests/continuationals/dot.con
-cic:/matita/tests/continuationals/dot_slice.con
-cic:/matita/tests/continuationals/focus.con
-cic:/matita/tests/continuationals/pos.con
-cic:/matita/tests/continuationals/semicolon.con
-cic:/matita/tests/continuationals/skip.con
-cic:/matita/tests/continuationals/skip_focus.con
-cic:/matita/tests/contradiction/stupid.con
-cic:/matita/tests/cut/stupid.con
-cic:/matita/tests/decl/easy15.con
-cic:/matita/tests/decl/easy2.con
-cic:/matita/tests/decl/easy3.con
-cic:/matita/tests/decl/easy45.con
-cic:/matita/tests/decl/easy4.con
-cic:/matita/tests/decl/easy5.con
-cic:/matita/tests/decl/easy6.con
-cic:/matita/tests/decl/easy.con
-cic:/matita/tests/decl/size.con
-cic:/matita/tests/decl/tree.ind
-cic:/matita/tests/decl/tree_ind.con
-cic:/matita/tests/decl/tree_rec.con
-cic:/matita/tests/decl/tree_rect.con
-cic:/matita/tests/decompose/ex_falso_quodlibet.con
-cic:/matita/tests/decompose/MyFalse.con
-cic:/matita/tests/decompose/stupid.con
-cic:/matita/tests/dependent_type_inference/foo.con
-cic:/matita/tests/elim/foo.con
-cic:/matita/tests/elim/serious.con
-cic:/matita/tests/elim/stupidtype.ind
-cic:/matita/tests/elim/stupidtype_ind.con
-cic:/matita/tests/elim/stupidtype_rec.con
-cic:/matita/tests/elim/stupidtype_rect.con
-cic:/matita/tests/elim/sum.ind
-cic:/matita/tests/elim/sum_ind.con
-cic:/matita/tests/elim/sum_inv.con
-cic:/matita/tests/elim/sum_rec.con
-cic:/matita/tests/elim/sum_rect.con
-cic:/matita/tests/elim/t.con
-cic:/matita/tests/elim/t'.con
-cic:/matita/tests/fguidi/eq_gen_S_O_cc.con
-cic:/matita/tests/fguidi/eq_gen_S_O.con
-cic:/matita/tests/fguidi/eq_gen_S_S_cc.con
-cic:/matita/tests/fguidi/eq_gen_S_S.con
-cic:/matita/tests/fguidi/is_S.con
-cic:/matita/tests/fguidi/le_gen_S_S_cc.con
-cic:/matita/tests/fguidi/le_gen_S_S.con
-cic:/matita/tests/fguidi/le_gen_S_x_aux.con
-cic:/matita/tests/fguidi/le_gen_S_x_cc.con
-cic:/matita/tests/fguidi/le_gen_S_x.con
-cic:/matita/tests/fguidi/le_gen_x_O_aux.con
-cic:/matita/tests/fguidi/le_gen_x_O_cc.con
-cic:/matita/tests/fguidi/le_gen_x_O.con
-cic:/matita/tests/fguidi/le.ind
-cic:/matita/tests/fguidi/le_ind.con
-cic:/matita/tests/fguidi/le_inv.con
-cic:/matita/tests/fguidi/le_refl.con
-cic:/matita/tests/fguidi/pred.con
-cic:/matita/tests/first/eq.ind
-cic:/matita/tests/first/eq_ind.con
-cic:/matita/tests/first/list.ind
-cic:/matita/tests/first/list_ind.con
-cic:/matita/tests/first/list_len.con
-cic:/matita/tests/first/list_rec.con
-cic:/matita/tests/first/list_rect.con
-cic:/matita/tests/first/nat.ind
-cic:/matita/tests/first/nat_ind.con
-cic:/matita/tests/first/nat_rec.con
-cic:/matita/tests/first/nat_rect.con
-cic:/matita/tests/first/stupid.con
-cic:/matita/tests/fix_betareduction/a.con
-cic:/matita/tests/fold/t.con
-cic:/matita/tests/generalize/t.con
-cic:/matita/tests/generalize/test2.con
-cic:/matita/tests/hard_refine/prove_add_multiply.con
-cic:/matita/tests/injection/injection_test0.con
-cic:/matita/tests/injection/injection_test1.con
-cic:/matita/tests/injection/injection_test2.con
-cic:/matita/tests/injection/injection_test4.con
-cic:/matita/tests/injection/t0.ind
-cic:/matita/tests/injection/t0_ind.con
-cic:/matita/tests/injection/t0_rec.con
-cic:/matita/tests/injection/t0_rect.con
-cic:/matita/tests/injection/t.ind
-cic:/matita/tests/injection/t_ind.con
-cic:/matita/tests/injection/t_inv.con
-cic:/matita/tests/injection/t_rec.con
-cic:/matita/tests/injection/t_rect.con
-cic:/matita/tests/injection/tt.ind
-cic:/matita/tests/injection/tt_ind.con
-cic:/matita/tests/injection/tt_inv.con
-cic:/matita/tests/injection/tt_rec.con
-cic:/matita/tests/injection/tt_rect.con
-cic:/matita/tests/injection/ttree.ind
-cic:/matita/tests/injection/ttree_ind.con
-cic:/matita/tests/injection/ttree_inv.con
-cic:/matita/tests/injection/ttree_rec.con
-cic:/matita/tests/injection/ttree_rect.con
-cic:/matita/tests/inversion2/ledx.ind
-cic:/matita/tests/inversion2/ledx_ind.con
-cic:/matita/tests/inversion2/ledx_inv.con
-cic:/matita/tests/inversion2/le.ind
-cic:/matita/tests/inversion2/le_ind.con
-cic:/matita/tests/inversion2/le_inv2.con
-cic:/matita/tests/inversion2/le_inv.con
-cic:/matita/tests/inversion2/nat.ind
-cic:/matita/tests/inversion2/nat_ind.con
-cic:/matita/tests/inversion2/nat_rec.con
-cic:/matita/tests/inversion2/nat_rect.con
-cic:/matita/tests/inversion2/test_inversion.con
-cic:/matita/tests/inversion/sum.ind
-cic:/matita/tests/inversion/sum_ind.con
-cic:/matita/tests/inversion/sum_inv.con
-cic:/matita/tests/inversion/sum_rec.con
-cic:/matita/tests/inversion/sum_rect.con
-cic:/matita/tests/inversion/t1.con
-cic:/matita/tests/inversion/t.con
-cic:/matita/tests/letrecand/dispari2.con
-cic:/matita/tests/letrecand/dispari.con
-cic:/matita/tests/letrecand/pari2.con
-cic:/matita/tests/letrecand/pari.con
-cic:/matita/tests/letrecand/test_dispari2.con
-cic:/matita/tests/letrecand/test_dispari.con
-cic:/matita/tests/letrecand/test_pari2.con
-cic:/matita/tests/letrecand/test_pari.con
-cic:/matita/tests/letrec/plus.con
-cic:/matita/tests/match_inference/empty2nat.con
-cic:/matita/tests/match_inference/empty.ind
-cic:/matita/tests/match_inference/empty_ind.con
-cic:/matita/tests/match_inference/empty_rec.con
-cic:/matita/tests/match_inference/empty_rect.con
-cic:/matita/tests/match_inference/fst.con
-cic:/matita/tests/match_inference/le.ind
-cic:/matita/tests/match_inference/le_ind.con
-cic:/matita/tests/match_inference/nat.ind
-cic:/matita/tests/match_inference/nat_ind.con
-cic:/matita/tests/match_inference/nat_rec.con
-cic:/matita/tests/match_inference/nat_rect.con
-cic:/matita/tests/match_inference/pos2nat.con
-cic:/matita/tests/match_inference/pos.ind
-cic:/matita/tests/match_inference/pos_ind.con
-cic:/matita/tests/match_inference/pos_rec.con
-cic:/matita/tests/match_inference/pos_rect.con
-cic:/matita/tests/match_inference/Prod.ind
-cic:/matita/tests/match_inference/Prod_ind.con
-cic:/matita/tests/match_inference/Prod_rec.con
-cic:/matita/tests/match_inference/Prod_rect.con
-cic:/matita/tests/match_inference/r.con
-cic:/matita/tests/match_inference/True.ind
-cic:/matita/tests/match_inference/True_ind.con
-cic:/matita/tests/match_inference/True_rec.con
-cic:/matita/tests/match_inference/True_rect.con
-cic:/matita/tests/metasenv_ordering/th10.con
-cic:/matita/tests/metasenv_ordering/th11.con
-cic:/matita/tests/metasenv_ordering/th1.con
-cic:/matita/tests/metasenv_ordering/th2.con
-cic:/matita/tests/metasenv_ordering/th3.con
-cic:/matita/tests/metasenv_ordering/th4.con
-cic:/matita/tests/metasenv_ordering/th5.con
-cic:/matita/tests/metasenv_ordering/th6.con
-cic:/matita/tests/metasenv_ordering/th7.con
-cic:/matita/tests/metasenv_ordering/th8.con
-cic:/matita/tests/metasenv_ordering/th9.con
-cic:/matita/tests/multiple_inheritance/C.con
-cic:/matita/tests/multiple_inheritance/conv_test.con
-cic:/matita/tests/multiple_inheritance/f.con
-cic:/matita/tests/multiple_inheritance/K.con
-cic:/matita/tests/multiple_inheritance/mult.con
-cic:/matita/tests/multiple_inheritance/mult_idempotent.con
-cic:/matita/tests/multiple_inheritance/plus.con
-cic:/matita/tests/multiple_inheritance/plus_idempotent.con
-cic:/matita/tests/multiple_inheritance/r1.con
-cic:/matita/tests/multiple_inheritance/R1.ind
-cic:/matita/tests/multiple_inheritance/R1_ind.con
-cic:/matita/tests/multiple_inheritance/R1_rec.con
-cic:/matita/tests/multiple_inheritance/R1_rect.con
-cic:/matita/tests/multiple_inheritance/r2_.con
-cic:/matita/tests/multiple_inheritance/r2.con
-cic:/matita/tests/multiple_inheritance/R2.ind
-cic:/matita/tests/multiple_inheritance/R2_ind.con
-cic:/matita/tests/multiple_inheritance/R2_rec.con
-cic:/matita/tests/multiple_inheritance/R2_rect.con
-cic:/matita/tests/multiple_inheritance/R.ind
-cic:/matita/tests/multiple_inheritance/R_ind.con
-cic:/matita/tests/multiple_inheritance/R_rec.con
-cic:/matita/tests/multiple_inheritance/R_rect.con
-cic:/matita/tests/multiple_inheritance/test.con
-cic:/matita/tests/multiple_inheritance/Type_OF_R.con
-cic:/matita/tests/multiple_inheritance/with_.con
-cic:/matita/tests/mysql_escaping/a'.con
-cic:/matita/tests/naiveparamod/prova1.con
-cic:/matita/tests/naiveparamod/prova2.con
-cic:/matita/tests/naiveparamod/TT.ind
-cic:/matita/tests/naiveparamod/TT_ind.con
-cic:/matita/tests/naiveparamod/TT_rec.con
-cic:/matita/tests/naiveparamod/TT_rect.con
-cic:/matita/tests/overred/c.con
-cic:/matita/tests/overred/daemon.con
-cic:/matita/tests/overred/find_a_coercion_from_T2_for_a_term_in_T3.con
-cic:/matita/tests/overred/T1.con
-cic:/matita/tests/overred/T2.con
-cic:/matita/tests/overred/t3.con
-cic:/matita/tests/overred/T3.con
-cic:/matita/tests/overred/x.con
-cic:/matita/tests/overred/X.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r'.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r''.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_f1.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_f.con
-cic:/matita/tests/paramodulation/BOO075-1/eq.ind
-cic:/matita/tests/paramodulation/BOO075-1/eq_ind.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_rec.con
-cic:/matita/tests/paramodulation/BOO075-1/eq_rect.con
-cic:/matita/tests/paramodulation/BOO075-1/ex.ind
-cic:/matita/tests/paramodulation/BOO075-1/ex_ind.con
-cic:/matita/tests/paramodulation/BOO075-1/prove_meredith_2_basis_1.con
-cic:/matita/tests/paramodulation/BOO075-1/sym_eq.con
-cic:/matita/tests/paramodulation/BOO075-1/trans_eq.con
-cic:/matita/tests/paramodulation/boolean_algebra/bool5.con
-cic:/matita/tests/paramodulation/boolean_algebra/bool_algebra.con
-cic:/matita/tests/paramodulation/group/GRP049.con
-cic:/matita/tests/paramodulation/group/GRP049_simple.con
-cic:/matita/tests/paramodulation/group/self.con
-cic:/matita/tests/paramodulation/para1.con
-cic:/matita/tests/paramodulation/para2.con
-cic:/matita/tests/pullback/L.ind
-cic:/matita/tests/pullback/L_ind.con
-cic:/matita/tests/pullback/L_OF_R1.con
-cic:/matita/tests/pullback/L_rec.con
-cic:/matita/tests/pullback/L_rect.con
-cic:/matita/tests/pullback/L_to_T.con
-cic:/matita/tests/pullback/P1.ind
-cic:/matita/tests/pullback/P1_ind.con
-cic:/matita/tests/pullback/P1_rec.con
-cic:/matita/tests/pullback/P1_rect.con
-cic:/matita/tests/pullback/P1_to_L.con
-cic:/matita/tests/pullback/P1_to_P1.con
-cic:/matita/tests/pullback/P1_to_R1.con
-cic:/matita/tests/pullback/P2.ind
-cic:/matita/tests/pullback/P2_ind.con
-cic:/matita/tests/pullback/P2_OF_P1.con
-cic:/matita/tests/pullback/P2_rec.con
-cic:/matita/tests/pullback/P2_rect.con
-cic:/matita/tests/pullback/P2_to_L.con
-cic:/matita/tests/pullback/P2_to_R.con
-cic:/matita/tests/pullback/R1.ind
-cic:/matita/tests/pullback/R1_ind.con
-cic:/matita/tests/pullback/R1_rec.con
-cic:/matita/tests/pullback/R1_rect.con
-cic:/matita/tests/pullback/R1_to_P2.con
-cic:/matita/tests/pullback/R1_to_R.con
-cic:/matita/tests/pullback/R.ind
-cic:/matita/tests/pullback/R_ind.con
-cic:/matita/tests/pullback/R_OF_P1.con
-cic:/matita/tests/pullback/R_rec.con
-cic:/matita/tests/pullback/R_rect.con
-cic:/matita/tests/pullback/R_to_T.con
-cic:/matita/tests/pullback/T.ind
-cic:/matita/tests/pullback/T_ind.con
-cic:/matita/tests/pullback/T_OF_P1.con
-cic:/matita/tests/pullback/T_OF_P2.con
-cic:/matita/tests/pullback/T_OF_R1.con
-cic:/matita/tests/pullback/T_rec.con
-cic:/matita/tests/pullback/T_rect.con
-cic:/matita/tests/record/a.con
-cic:/matita/tests/record/b.con
-cic:/matita/tests/record/c.con
-cic:/matita/tests/record/d.con
-cic:/matita/tests/record/e.con
-cic:/matita/tests/record/empty.ind
-cic:/matita/tests/record/empty_ind.con
-cic:/matita/tests/record/empty_rec.con
-cic:/matita/tests/record/empty_rect.con
-cic:/matita/tests/record/f.con
-cic:/matita/tests/record/mario.con
-cic:/matita/tests/record/paperino.ind
-cic:/matita/tests/record/paperino_ind.con
-cic:/matita/tests/record/piero.con
-cic:/matita/tests/record/pippo.ind
-cic:/matita/tests/record/pippo_ind.con
-cic:/matita/tests/record/pippo_rec.con
-cic:/matita/tests/record/pippo_rect.con
-cic:/matita/tests/record/pluto.ind
-cic:/matita/tests/record/pluto_ind.con
-cic:/matita/tests/record/pluto_rec.con
-cic:/matita/tests/record/pluto_rect.con
-cic:/matita/tests/record/t.ind
-cic:/matita/tests/record/t_ind.con
-cic:/matita/tests/record/t_rec.con
-cic:/matita/tests/record/t_rect.con
-cic:/matita/tests/record/True.ind
-cic:/matita/tests/record/True_ind.con
-cic:/matita/tests/record/True_rec.con
-cic:/matita/tests/record/True_rect.con
-cic:/matita/tests/replace/t2.con
-cic:/matita/tests/replace/t.con
-cic:/matita/tests/rewrite/a.con
-cic:/matita/tests/rewrite/foo.con
-cic:/matita/tests/rewrite/t.con
-cic:/matita/tests/rewrite/test_rewrite_in_hyp2.con
-cic:/matita/tests/rewrite/test_rewrite_in_hyp.con
-cic:/matita/tests/rewrite/test_rewrite_under_pi.con
-cic:/matita/tests/second/ultrastupid.con
-cic:/matita/tests/simpl/R.con
-cic:/matita/tests/simpl/t.con
-cic:/matita/tests/simpl/X.con
-cic:/matita/tests/tacticals/myand.ind
-cic:/matita/tests/tacticals/myand_ind.con
-cic:/matita/tests/tacticals/myand_rec.con
-cic:/matita/tests/tacticals/myand_rect.con
-cic:/matita/tests/tacticals/prova2.con
-cic:/matita/tests/tacticals/prova3.con
-cic:/matita/tests/tacticals/prova4.con
-cic:/matita/tests/tacticals/prova6.con
-cic:/matita/tests/tacticals/prova.con
-cic:/matita/tests/test2/a.con
-cic:/matita/tests/test3/a.con
-cic:/matita/tests/test3/b.con
-cic:/matita/tests/test4/a.con
-cic:/matita/tests/third/iperstupid.con
-cic:/matita/tests/tinycals/prova1.con
-cic:/matita/tests/tinycals/prova2.con
-cic:/matita/tests/tinycals/prova.con
-cic:/matita/tests/TPTP/Veloci/BOO001-1.p/prove_inverse_is_self_cancelling.con
-cic:/matita/tests/TPTP/Veloci/BOO003-2.p/prove_a_times_a_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO003-4.p/prove_a_times_a_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO004-2.p/prove_a_plus_a_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO004-4.p/prove_a_plus_a_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO005-2.p/prove_a_plus_1_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO005-4.p/prove_a_plus_1_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO006-2.p/prove_right_identity.con
-cic:/matita/tests/TPTP/Veloci/BOO006-4.p/prove_right_identity.con
-cic:/matita/tests/TPTP/Veloci/BOO009-2.p/prove_operation.con
-cic:/matita/tests/TPTP/Veloci/BOO009-4.p/prove_operation.con
-cic:/matita/tests/TPTP/Veloci/BOO010-2.p/prove_a_plus_ab_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO010-4.p/prove_a_plus_ab_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO011-2.p/prove_inverse_of_1_is_0.con
-cic:/matita/tests/TPTP/Veloci/BOO011-4.p/prove_inverse_of_1_is_0.con
-cic:/matita/tests/TPTP/Veloci/BOO012-2.p/prove_inverse_is_an_involution.con
-cic:/matita/tests/TPTP/Veloci/BOO012-4.p/prove_inverse_is_an_involution.con
-cic:/matita/tests/TPTP/Veloci/BOO013-2.p/prove_b_is_a.con
-cic:/matita/tests/TPTP/Veloci/BOO013-4.p/prove_a_inverse_is_b.con
-cic:/matita/tests/TPTP/Veloci/BOO016-2.p/prove_sum.con
-cic:/matita/tests/TPTP/Veloci/BOO017-2.p/prove_sum.con
-cic:/matita/tests/TPTP/Veloci/BOO018-4.p/prove_inverse_of_1_is_0.con
-cic:/matita/tests/TPTP/Veloci/BOO034-1.p/prove_single_axiom.con
-cic:/matita/tests/TPTP/Veloci/BOO069-1.p/prove_tba_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/BOO071-1.p/prove_tba_axioms_5.con
-cic:/matita/tests/TPTP/Veloci/BOO075-1.p/prove_meredith_2_basis_1.con
-cic:/matita/tests/TPTP/Veloci/COL004-3.p/prove_u_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL007-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL008-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL010-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL012-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL013-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL014-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL015-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL016-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL017-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL018-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL021-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL022-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL024-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL025-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL045-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL048-1.p/prove_fixed_point.con
-cic:/matita/tests/TPTP/Veloci/COL050-1.p/prove_all_fond_of_another.con
-cic:/matita/tests/TPTP/Veloci/COL058-2.p/prove_the_bird_exists.con
-cic:/matita/tests/TPTP/Veloci/COL058-3.p/prove_the_bird_exists.con
-cic:/matita/tests/TPTP/Veloci/COL060-2.p/prove_q_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL060-3.p/prove_q_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL061-2.p/prove_q1_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL061-3.p/prove_q1_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL062-2.p/prove_c_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL062-3.p/prove_c_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL063-2.p/prove_f_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL063-3.p/prove_f_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL063-4.p/prove_f_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL063-5.p/prove_f_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL063-6.p/prove_f_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-2.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-3.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-4.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-5.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-6.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-7.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-8.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/COL064-9.p/prove_v_combinator.con
-cic:/matita/tests/TPTP/Veloci/GRP001-2.p/prove_b_times_a_is_c.con
-cic:/matita/tests/TPTP/Veloci/GRP001-4.p/prove_b_times_a_is_c.con
-cic:/matita/tests/TPTP/Veloci/GRP010-4.p/prove_b_times_c_is_e.con
-cic:/matita/tests/TPTP/Veloci/GRP011-4.p/prove_left_cancellation.con
-cic:/matita/tests/TPTP/Veloci/GRP012-4.p/prove_inverse_of_product_is_product_of_inverses.con
-cic:/matita/tests/TPTP/Veloci/GRP022-2.p/prove_inverse_of_inverse_is_original.con
-cic:/matita/tests/TPTP/Veloci/GRP023-2.p/prove_inverse_of_id_is_id.con
-cic:/matita/tests/TPTP/Veloci/GRP115-1.p/prove_order3.con
-cic:/matita/tests/TPTP/Veloci/GRP116-1.p/prove_order3.con
-cic:/matita/tests/TPTP/Veloci/GRP117-1.p/prove_order3.con
-cic:/matita/tests/TPTP/Veloci/GRP118-1.p/prove_order3.con
-cic:/matita/tests/TPTP/Veloci/GRP136-1.p/prove_ax_antisyma.con
-cic:/matita/tests/TPTP/Veloci/GRP137-1.p/prove_ax_antisymb.con
-cic:/matita/tests/TPTP/Veloci/GRP139-1.p/prove_ax_glb1b.con
-cic:/matita/tests/TPTP/Veloci/GRP141-1.p/prove_ax_glb1d.con
-cic:/matita/tests/TPTP/Veloci/GRP142-1.p/prove_ax_glb2a.con
-cic:/matita/tests/TPTP/Veloci/GRP143-1.p/prove_ax_glb2b.con
-cic:/matita/tests/TPTP/Veloci/GRP144-1.p/prove_ax_glb3a.con
-cic:/matita/tests/TPTP/Veloci/GRP145-1.p/prove_ax_glb3b.con
-cic:/matita/tests/TPTP/Veloci/GRP146-1.p/prove_ax_lub1a.con
-cic:/matita/tests/TPTP/Veloci/GRP149-1.p/prove_ax_lub1d.con
-cic:/matita/tests/TPTP/Veloci/GRP150-1.p/prove_ax_lub2a.con
-cic:/matita/tests/TPTP/Veloci/GRP151-1.p/prove_ax_lub2b.con
-cic:/matita/tests/TPTP/Veloci/GRP152-1.p/prove_ax_lub3a.con
-cic:/matita/tests/TPTP/Veloci/GRP153-1.p/prove_ax_lub3b.con
-cic:/matita/tests/TPTP/Veloci/GRP154-1.p/prove_ax_mono1a.con
-cic:/matita/tests/TPTP/Veloci/GRP155-1.p/prove_ax_mono1b.con
-cic:/matita/tests/TPTP/Veloci/GRP156-1.p/prove_ax_mono1c.con
-cic:/matita/tests/TPTP/Veloci/GRP157-1.p/prove_ax_mono2a.con
-cic:/matita/tests/TPTP/Veloci/GRP158-1.p/prove_ax_mono2b.con
-cic:/matita/tests/TPTP/Veloci/GRP159-1.p/prove_ax_mono2c.con
-cic:/matita/tests/TPTP/Veloci/GRP160-1.p/prove_ax_refla.con
-cic:/matita/tests/TPTP/Veloci/GRP161-1.p/prove_ax_reflb.con
-cic:/matita/tests/TPTP/Veloci/GRP162-1.p/prove_ax_transa.con
-cic:/matita/tests/TPTP/Veloci/GRP163-1.p/prove_ax_transb.con
-cic:/matita/tests/TPTP/Veloci/GRP168-1.p/prove_p01a.con
-cic:/matita/tests/TPTP/Veloci/GRP168-2.p/prove_p01b.con
-cic:/matita/tests/TPTP/Veloci/GRP173-1.p/prove_p05a.con
-cic:/matita/tests/TPTP/Veloci/GRP174-1.p/prove_p05b.con
-cic:/matita/tests/TPTP/Veloci/GRP176-1.p/prove_p07.con
-cic:/matita/tests/TPTP/Veloci/GRP176-2.p/prove_p07.con
-cic:/matita/tests/TPTP/Veloci/GRP182-1.p/prove_p17a.con
-cic:/matita/tests/TPTP/Veloci/GRP182-2.p/prove_p17a.con
-cic:/matita/tests/TPTP/Veloci/GRP182-3.p/prove_p17b.con
-cic:/matita/tests/TPTP/Veloci/GRP182-4.p/prove_p17b.con
-cic:/matita/tests/TPTP/Veloci/GRP186-3.p/prove_p23x.con
-cic:/matita/tests/TPTP/Veloci/GRP186-4.p/prove_p23x.con
-cic:/matita/tests/TPTP/Veloci/GRP188-1.p/prove_p38a.con
-cic:/matita/tests/TPTP/Veloci/GRP188-2.p/prove_p38a.con
-cic:/matita/tests/TPTP/Veloci/GRP189-1.p/prove_p38b.con
-cic:/matita/tests/TPTP/Veloci/GRP189-2.p/prove_p38b.con
-cic:/matita/tests/TPTP/Veloci/GRP192-1.p/prove_p40a.con
-cic:/matita/tests/TPTP/Veloci/GRP206-1.p/prove_moufang1.con
-cic:/matita/tests/TPTP/Veloci/GRP454-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP455-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP456-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP457-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP458-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP459-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP460-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP463-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP467-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP481-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP484-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP485-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP486-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP487-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP488-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP490-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP491-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP492-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP493-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP494-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP495-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP496-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP497-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP498-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP509-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP510-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP511-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP512-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP513-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP514-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP515-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP516-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP517-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP518-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP520-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP541-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP542-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP543-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP544-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP545-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP546-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP547-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP548-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP549-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP550-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP551-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP552-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP556-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP558-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP560-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP561-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP562-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP564-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP565-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP566-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP567-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP568-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP569-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP570-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP572-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP573-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP574-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP576-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP577-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP578-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP580-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP581-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP582-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP583-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP584-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP586-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP588-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP590-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP592-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP595-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP596-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP597-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP598-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP599-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP600-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP602-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP603-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP604-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP605-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP606-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP608-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP612-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/GRP613-1.p/prove_these_axioms_1.con
-cic:/matita/tests/TPTP/Veloci/GRP614-1.p/prove_these_axioms_2.con
-cic:/matita/tests/TPTP/Veloci/GRP615-1.p/prove_these_axioms_3.con
-cic:/matita/tests/TPTP/Veloci/GRP616-1.p/prove_these_axioms_4.con
-cic:/matita/tests/TPTP/Veloci/LAT008-1.p/prove_absorbtion_dual.con
-cic:/matita/tests/TPTP/Veloci/LAT033-1.p/idempotence_of_join.con
-cic:/matita/tests/TPTP/Veloci/LAT034-1.p/idempotence_of_meet.con
-cic:/matita/tests/TPTP/Veloci/LAT039-1.p/rhs.con
-cic:/matita/tests/TPTP/Veloci/LAT039-2.p/rhs.con
-cic:/matita/tests/TPTP/Veloci/LAT040-1.p/rhs.con
-cic:/matita/tests/TPTP/Veloci/LAT045-1.p/prove_orthomodular_law.con
-cic:/matita/tests/TPTP/Veloci/LCL110-2.p/prove_mv_24.con
-cic:/matita/tests/TPTP/Veloci/LCL112-2.p/prove_mv_29.con
-cic:/matita/tests/TPTP/Veloci/LCL113-2.p/prove_mv_33.con
-cic:/matita/tests/TPTP/Veloci/LCL114-2.p/prove_mv_36.con
-cic:/matita/tests/TPTP/Veloci/LCL115-2.p/prove_mv_39.con
-cic:/matita/tests/TPTP/Veloci/LCL132-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL133-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL134-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL135-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL139-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL140-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL141-1.p/prove_wajsberg_lemma.con
-cic:/matita/tests/TPTP/Veloci/LCL153-1.p/prove_alternative_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL154-1.p/prove_alternative_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL155-1.p/prove_alternative_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL156-1.p/prove_alternative_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL157-1.p/prove_alternative_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL158-1.p/prove_alternative_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL161-1.p/prove_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LCL164-1.p/prove_wajsberg_axiom.con
-cic:/matita/tests/TPTP/Veloci/LDA001-1.p/prove_equation.con
-cic:/matita/tests/TPTP/Veloci/LDA007-3.p/prove_equation.con
-cic:/matita/tests/TPTP/Veloci/RNG007-4.p/prove_inverse.con
-cic:/matita/tests/TPTP/Veloci/RNG008-4.p/prove_commutativity.con
-cic:/matita/tests/TPTP/Veloci/RNG011-5.p/prove_equality.con
-cic:/matita/tests/TPTP/Veloci/RNG023-6.p/prove_left_alternative.con
-cic:/matita/tests/TPTP/Veloci/RNG023-7.p/prove_left_alternative.con
-cic:/matita/tests/TPTP/Veloci/RNG024-6.p/prove_right_alternative.con
-cic:/matita/tests/TPTP/Veloci/RNG024-7.p/prove_right_alternative.con
-cic:/matita/tests/TPTP/Veloci/ROB002-1.p/prove_huntingtons_axiom.con
-cic:/matita/tests/TPTP/Veloci/ROB009-1.p/prove_result.con
-cic:/matita/tests/TPTP/Veloci/ROB010-1.p/prove_result.con
-cic:/matita/tests/TPTP/Veloci/ROB013-1.p/prove_result.con
-cic:/matita/tests/TPTP/Veloci/ROB030-1.p/prove_absorption_within_negation.con
-cic:/matita/tests/TPTP/Veloci/SYN083-1.p/prove_this.con
-cic:/matita/tests/unfold/lem.con
-cic:/matita/tests/unfold/myplus.con
-cic:/matita/tests/unfold/t.con
-cic:/matita/tests/unfold/trivial.con
+cic:/Lyon/FIRING-SQUAD/basic/GC_dollarB.con
+cic:/Lyon/FIRING-SQUAD/basic/GC_G.con
+cic:/Marseille/GC/card/card/card.ind
+cic:/Marseille/GC/card/card/card_ind.con
+cic:/Marseille/GC/card/card/card_inv.con
+cic:/Marseille/GC/card/card/card_rem.con
+cic:/Marseille/GC/card/card/dif2.con
+cic:/Marseille/GC/card/card/dif.con
+cic:/Marseille/GC/card/card/eq_dec_set.con
+cic:/Marseille/GC/card/card/exist_updated.con
+cic:/Marseille/GC/card/card_facts/eq_dec_set.con
+cic:/Marseille/GC/card/card_facts/exist_updated_M.con
+cic:/Marseille/GC/card/card_facts/exist_updated_N.con
+cic:/Marseille/GC/card/card_facts/include_card_bis.con
+cic:/Marseille/GC/card/card_facts/include_card.con
+cic:/Marseille/GC/card/card_facts/prop_dec2.con
+cic:/Marseille/GC/card/card_facts/prop_dec.con
+cic:/Marseille/GC/card/card_facts/update_M.con
+cic:/Marseille/GC/card/card_facts/update_N.con
+cic:/Marseille/GC/card/card/unicity_card.con
+cic:/Marseille/GC/card/card/update.con
+cic:/Marseille/GC/gc/gc/acc_imp_notfree.con
+cic:/Marseille/GC/gc/gc/add.con
+cic:/Marseille/GC/gc/gc/add_edge.ind
+cic:/Marseille/GC/gc/gc/add_edge_ind.con
+cic:/Marseille/GC/gc/gc/alloc.ind
+cic:/Marseille/GC/gc/gc/alloc_ind.con
+cic:/Marseille/GC/gc/gc/cases_marknode.con
+cic:/Marseille/GC/gc/gc/fair.con
+cic:/Marseille/GC/gc/gc/gc_call.ind
+cic:/Marseille/GC/gc/gc/gc_call_ind.con
+cic:/Marseille/GC/gc/gc/gc_end.ind
+cic:/Marseille/GC/gc/gc/gc_end_ind.con
+cic:/Marseille/GC/gc/gc/gc_end_rec.con
+cic:/Marseille/GC/gc/gc/gc_end_rect.con
+cic:/Marseille/GC/gc/gc/gc_free1.ind
+cic:/Marseille/GC/gc/gc/gc_free1_ind.con
+cic:/Marseille/GC/gc/gc/gc_free.ind
+cic:/Marseille/GC/gc/gc/gc_free_ind.con
+cic:/Marseille/GC/gc/gc/gc_stop.ind
+cic:/Marseille/GC/gc/gc/gc_stop_ind.con
+cic:/Marseille/GC/gc/gc/gc_stop_rec.con
+cic:/Marseille/GC/gc/gc/gc_stop_rect.con
+cic:/Marseille/GC/gc/gc/grey_node_case.ind
+cic:/Marseille/GC/gc/gc/grey_node_case_ind.con
+cic:/Marseille/GC/gc/gc/init_color.con
+cic:/Marseille/GC/gc/gc/init_marking.con
+cic:/Marseille/GC/gc/gc/init_state.con
+cic:/Marseille/GC/gc/gc/label.ind
+cic:/Marseille/GC/gc/gc/label_ind.con
+cic:/Marseille/GC/gc/gc/label_rec.con
+cic:/Marseille/GC/gc/gc/label_rect.con
+cic:/Marseille/GC/gc/gc/marking_add.con
+cic:/Marseille/GC/gc/gc/mark_node.ind
+cic:/Marseille/GC/gc/gc/mark_node_ind.con
+cic:/Marseille/GC/gc/gc/mark_node_rec.con
+cic:/Marseille/GC/gc/gc/mark_node_rect.con
+cic:/Marseille/GC/gc/gc/no_edge_black_to_white_bis.con
+cic:/Marseille/GC/gc/gc/no_edge_black_to_white.con
+cic:/Marseille/GC/gc/gc/nogrey_accn_imp_blackn.con
+cic:/Marseille/GC/gc/gc/remove.con
+cic:/Marseille/GC/gc/gc/remove_edge.ind
+cic:/Marseille/GC/gc/gc/remove_edge_ind.con
+cic:/Marseille/GC/gc/gc/rt_grey_or_black.con
+cic:/Marseille/GC/gc/gc/sweep_no_greys.con
+cic:/Marseille/GC/gc/gc/transition.ind
+cic:/Marseille/GC/gc/gc/transition_ind.con
+cic:/Marseille/GC/gc/gc/update_color.con
+cic:/Marseille/GC/gc/parameters/color.ind
+cic:/Marseille/GC/gc/parameters/color_ind.con
+cic:/Marseille/GC/gc/parameters/color_rec.con
+cic:/Marseille/GC/gc/parameters/color_rect.con
+cic:/Marseille/GC/gc/parameters/control.ind
+cic:/Marseille/GC/gc/parameters/control_ind.con
+cic:/Marseille/GC/gc/parameters/control_rec.con
+cic:/Marseille/GC/gc/parameters/control_rect.con
+cic:/Marseille/GC/gc/parameters/ctl.con
+cic:/Marseille/GC/gc/parameters/eq_dec_color.con
+cic:/Marseille/GC/gc/parameters/eq_dec_node.con
+cic:/Marseille/GC/gc/parameters/heap.con
+cic:/Marseille/GC/gc/parameters/hp.con
+cic:/Marseille/GC/gc/parameters/marking.con
+cic:/Marseille/GC/gc/parameters/mk.con
+cic:/Marseille/GC/gc/parameters/node.con
+cic:/Marseille/GC/gc/parameters/noteqmar_noteqnod.con
+cic:/Marseille/GC/gc/parameters/rt.con
+cic:/Marseille/GC/gc/parameters/state.ind
+cic:/Marseille/GC/gc/parameters/state_ind.con
+cic:/Marseille/GC/gc/parameters/state_rec.con
+cic:/Marseille/GC/gc/parameters/state_rect.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_ancestor.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_notacc_white.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_notgreyt_notgreys.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_add/add_white_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_ancestor.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_greys_greyt.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_notgreys_notgreyt.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_notgreyt_notgreys.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_notwhites_notwhitet.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_alloc/alloc_whites_whitet.con
+cic:/Marseille/GC/lemma_step/lemma_call/gccall_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_notgreyt_notgreys.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_end/gcend_white.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_greys_greyt.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_notblacks_notblackt.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_notgreys_notgreyt.con
+cic:/Marseille/GC/lemma_step/lemma_free1/gcfree1_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_greys_greyt.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_notblacks_notblackt.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_notgreys_notgreyt.con
+cic:/Marseille/GC/lemma_step/lemma_free/gcfree_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_free/updatecolor_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_mark/grey_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_mark/greynode_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_mark/grey_white.con
+cic:/Marseille/GC/lemma_step/lemma_mark/mark_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_mark/mark_ancestor.con
+cic:/Marseille/GC/lemma_step/lemma_mark/marknode_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_mark/marknode_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_mark/marknode_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_mark/mark_white.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_ancestor.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_notgreyt_notgreys.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_remove/remove_white.con
+cic:/Marseille/GC/lemma_step/lemma_step/color_node.con
+cic:/Marseille/GC/lemma_step/lemma_step/ind.con
+cic:/Marseille/GC/lemma_step/lemma_step/initcolor_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_step/trivial.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_accest_access.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_ancestor_col.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_blacks_blackt.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_nogrey.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_notaccess_notaccest.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_notfrees_notfreet.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_notgreyt_notgreys.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_nowhite.con
+cic:/Marseille/GC/lemma_step/lemma_stop/gcstop_white.con
+cic:/Marseille/GC/lib_arith/lib_minus/minus_pred.con
+cic:/Marseille/GC/lib_arith/lib_minus/pred_S_minus.con
+cic:/Marseille/GC/lib_arith/lib_plus/plus_O.con
+cic:/Marseille/GC/lib_arith/lib_plus/plus_O_O.con
+cic:/Marseille/GC/lib_arith/lib_plus/plus_pred.con
+cic:/Marseille/GC/lib_arith/lib_plus/plus_S_pred.con
+cic:/Marseille/GC/lib_arith/lib_plus/pred_plus_minus.con
+cic:/Marseille/GC/lib_arith/lib_plus/pred_plus_S.con
+cic:/Marseille/GC/lib_arith/lib_S_pred/eqnm_eqSnSm.con
+cic:/Marseille/GC/lib_arith/lib_S_pred/pred_S.con
+cic:/Marseille/GC/lib_arith/lib_S_pred/S_pred.con
+cic:/Marseille/GC/liveness/fairstr/always_exist_fairstep.con
+cic:/Marseille/GC/liveness/fairstr/always_fairstep.con
+cic:/Marseille/GC/liveness/fairstr/call_exist_grey_fair.con
+cic:/Marseille/GC/liveness/fairstr/call_gc_fair.con
+cic:/Marseille/GC/liveness/fairstr/exist_grey_node.con
+cic:/Marseille/GC/liveness/fairstr/exist_or_none.con
+cic:/Marseille/GC/liveness/fairstr/exist_update_color.con
+cic:/Marseille/GC/liveness/fairstr/exist_update_init_color.con
+cic:/Marseille/GC/liveness/fairstr/fairstr_eventually.con
+cic:/Marseille/GC/liveness/fairstr/fairstr_eventually_tl.con
+cic:/Marseille/GC/liveness/fairstr/free1_white_fair.con
+cic:/Marseille/GC/liveness/fairstr/gcfree_fair.con
+cic:/Marseille/GC/liveness/fairstr/infinitely_fairstep.con
+cic:/Marseille/GC/liveness/fairstr/marknode_fair.con
+cic:/Marseille/GC/liveness/fairstr/no_grey_but_white_fair.con
+cic:/Marseille/GC/liveness/fairstr/update_color_marknode.con
+cic:/Marseille/GC/liveness/fairstr/update_init_color.con
+cic:/Marseille/GC/liveness/liveness/always_and_inv_g_w_b.con
+cic:/Marseille/GC/liveness/liveness/and_inv.con
+cic:/Marseille/GC/liveness/liveness/card_grey_rt.con
+cic:/Marseille/GC/liveness/liveness/def_equiv.con
+cic:/Marseille/GC/liveness/liveness/liveness.con
+cic:/Marseille/GC/liveness/liveness/run_fairstr_always.con
+cic:/Marseille/GC/liveness/liveness/safe_inv_and_gwb.con
+cic:/Marseille/GC/liveness/liveness/safe_inv_gwb_mesure.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/add_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/alloc_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/equiv_def2.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/equiv_def.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/gccall_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/gcend_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/gcfree1_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/gcfree_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/gcstop_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/marknode_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/notacc_black_nogrey_exwhite.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/notacc_black_nogrey_exwhite_formula.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/notacc_black_nogrey_formula.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/notacc_black_nogrey_nowhite_formula.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/notacc_black_nomeasure_formula.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/remove_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/step_notacc_black_nogrey.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/until_no_measure.con
+cic:/Marseille/GC/liveness/notacc_black_nogrey/until_no_white.con
+cic:/Marseille/GC/liveness/notacc_init/add_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/alloc_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/fairstep_implies_gc_call.con
+cic:/Marseille/GC/liveness/notacc_init/fairstep_implies_initcol.con
+cic:/Marseille/GC/liveness/notacc_init/gccall_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/gcend_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/gcfree1_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/gcfree_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/gcstop_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/init_implies_whiteorfree.con
+cic:/Marseille/GC/liveness/notacc_init/marknode_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/notacc_black_nomeasure.con
+cic:/Marseille/GC/liveness/notacc_init/notacc_black_nomeasure_formula.con
+cic:/Marseille/GC/liveness/notacc_init/notacc_white_init.con
+cic:/Marseille/GC/liveness/notacc_init/notacc_white_init_formula.con
+cic:/Marseille/GC/liveness/notacc_init/null_measure_grey_white.con
+cic:/Marseille/GC/liveness/notacc_init/remove_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/step_idem_or_init.con
+cic:/Marseille/GC/liveness/notacc_init/step_initcolor.con
+cic:/Marseille/GC/liveness/notacc_init/until_no_measure_init.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/add_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/alloc_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/equivalent_def.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/gccall_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/gcend_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/gcfree1_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/gcfree_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/gcstop_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/mark_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/notacc_white_exgrey_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/notacc_white_exgrey_reach_formula.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/notacc_white_nogrey_eventually_free.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/notacc_white_reach_formula.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/remove_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/step_notacc_white_reach.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/until_no_grey.con
+cic:/Marseille/GC/liveness/notacc_white_ancestor/until_no_grey_without_reach.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/add_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/alloc_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/gccall_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/gcend_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/gcfree1_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/gcfree_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/gcstop_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/mark_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/notacc_white_nogrey.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/notacc_white_nogrey_formula.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/notacc_white_nogrey_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/remove_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/step_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/until_idem_or_free.con
+cic:/Marseille/GC/liveness/notacc_white_nogrey/white_notacc_nogrey_until_eventually_free.con
+cic:/Marseille/GC/liveness/notfree_notacc/addedge_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/alloc_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/always_notfree_notacces_unless_isfree.con
+cic:/Marseille/GC/liveness/notfree_notacc/free_or_notfree_notacc_nogrey.con
+cic:/Marseille/GC/liveness/notfree_notacc/gccall_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/gcend_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/gcfree1_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/gcfree_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/gcstop_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/is_free.con
+cic:/Marseille/GC/liveness/notfree_notacc/marknode_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/notfree.con
+cic:/Marseille/GC/liveness/notfree_notacc/notfree_notacces.con
+cic:/Marseille/GC/liveness/notfree_notacc/notfree_notacces_unless_isfree.con
+cic:/Marseille/GC/liveness/notfree_notacc/removeedge_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/step_notacces_t.con
+cic:/Marseille/GC/liveness/notfree_notacc/until_free_or_nogrey.con
+cic:/Marseille/GC/liveness/until_zero/always_eventually_grey_until_zero_trace.con
+cic:/Marseille/GC/liveness/until_zero/always_eventually_white_until_zero_trace.con
+cic:/Marseille/GC/liveness/until_zero/and_exist.con
+cic:/Marseille/GC/liveness/until_zero/eventually_grey_until_zero.con
+cic:/Marseille/GC/liveness/until_zero/eventually_grey_until_zero_trace.con
+cic:/Marseille/GC/liveness/until_zero/eventually_measure_until_zero.con
+cic:/Marseille/GC/liveness/until_zero/eventually_measure_until_zero_on_run.con
+cic:/Marseille/GC/liveness/until_zero/eventually_measure_until_zero_trace_bis.con
+cic:/Marseille/GC/liveness/until_zero/eventually_measure_until_zero_trace.con
+cic:/Marseille/GC/liveness/until_zero/eventually_white_until_zero.con
+cic:/Marseille/GC/liveness/until_zero/eventually_white_until_zero_trace.con
+cic:/Marseille/GC/liveness/until_zero/fairness_decrease.con
+cic:/Marseille/GC/liveness/until_zero/fairness_lt.con
+cic:/Marseille/GC/liveness/until_zero/le_measure.con
+cic:/Marseille/GC/liveness/until_zero/measure.con
+cic:/Marseille/GC/liveness/until_zero/measureO_greyO.con
+cic:/Marseille/GC/liveness/until_zero/measureO_whiteO.con
+cic:/Marseille/GC/liveness/until_zero/measure_trivial_bis.con
+cic:/Marseille/GC/liveness/until_zero/measure_trivial.con
+cic:/Marseille/GC/liveness/until_zero/measure_until_zero.con
+cic:/Marseille/GC/liveness/until_zero/measure_until_zero_on_run.con
+cic:/Marseille/GC/liveness/until_zero/none_or_one_decrease.con
+cic:/Marseille/GC/liveness/until_zero/once_until_zero.con
+cic:/Marseille/GC/liveness/until_zero/positive_measure.con
+cic:/Marseille/GC/liveness/until_zero/step_decrease.con
+cic:/Marseille/GC/liveness/until_zero/trivial_unicity_bis.con
+cic:/Marseille/GC/liveness/until_zero/trivial_unicity.con
+cic:/Marseille/GC/liveness/until_zero/until_zero.con
+cic:/Marseille/GC/logique/LTL/always_always_bis.con
+cic:/Marseille/GC/logique/LTL/always_always.con
+cic:/Marseille/GC/logique/LTL/always_always_implies_always.con
+cic:/Marseille/GC/logique/LTL/always_and_and.con
+cic:/Marseille/GC/logique/LTL/always_and_bis.con
+cic:/Marseille/GC/logique/LTL/always_and.con
+cic:/Marseille/GC/logique/LTL/always_fairstr.con
+cic:/Marseille/GC/logique/LTL/always_imp_always.con
+cic:/Marseille/GC/logique/LTL/always_implies_always.con
+cic:/Marseille/GC/logique/LTL/always_implies_always_state.con
+cic:/Marseille/GC/logique/LTL/always_implies_always_stream.con
+cic:/Marseille/GC/logique/LTL/always.ind
+cic:/Marseille/GC/logique/LTL/always_one_step_leads_to.con
+cic:/Marseille/GC/logique/LTL/always_on_run.con
+cic:/Marseille/GC/logique/LTL/always_P.con
+cic:/Marseille/GC/logique/LTL/always_trace.con
+cic:/Marseille/GC/logique/LTL/always_unless.con
+cic:/Marseille/GC/logique/LTL/and_always.con
+cic:/Marseille/GC/logique/LTL/and_always_state.con
+cic:/Marseille/GC/logique/LTL/and.con
+cic:/Marseille/GC/logique/LTL/and_state.con
+cic:/Marseille/GC/logique/LTL/enabled.ind
+cic:/Marseille/GC/logique/LTL/enabled_ind.con
+cic:/Marseille/GC/logique/LTL/eventually_implies_eventually.con
+cic:/Marseille/GC/logique/LTL/Eventually.ind
+cic:/Marseille/GC/logique/LTL/Eventually_ind.con
+cic:/Marseille/GC/logique/LTL/Eventually_permanently.con
+cic:/Marseille/GC/logique/LTL/eventually_until.con
+cic:/Marseille/GC/logique/LTL/fairness.con
+cic:/Marseille/GC/logique/LTL/fair_step.ind
+cic:/Marseille/GC/logique/LTL/fair_step_ind.con
+cic:/Marseille/GC/logique/LTL/fairstr.con
+cic:/Marseille/GC/logique/LTL/followed_until.con
+cic:/Marseille/GC/logique/LTL/head_str.con
+cic:/Marseille/GC/logique/LTL/implies.con
+cic:/Marseille/GC/logique/LTL/implies_inf_often.con
+cic:/Marseille/GC/logique/LTL/induct.con
+cic:/Marseille/GC/logique/LTL/infinitely_often.con
+cic:/Marseille/GC/logique/LTL/invariant.con
+cic:/Marseille/GC/logique/LTL/inv_clos.con
+cic:/Marseille/GC/logique/LTL/inv_implies_inf_often.con
+cic:/Marseille/GC/logique/LTL/is_always_followed.con
+cic:/Marseille/GC/logique/LTL/is_followed.con
+cic:/Marseille/GC/logique/LTL/leads_to.con
+cic:/Marseille/GC/logique/LTL/leadsto_tx_l_or.con
+cic:/Marseille/GC/logique/LTL/leads_to_via.con
+cic:/Marseille/GC/logique/LTL/ltv_equiv_ltv.con
+cic:/Marseille/GC/logique/LTL/next.con
+cic:/Marseille/GC/logique/LTL/none_or_one_step.ind
+cic:/Marseille/GC/logique/LTL/none_or_one_step_ind.con
+cic:/Marseille/GC/logique/LTL/once_always.con
+cic:/Marseille/GC/logique/LTL/once_equiv_once.con
+cic:/Marseille/GC/logique/LTL/once_eventually.con
+cic:/Marseille/GC/logique/LTL/once_until.con
+cic:/Marseille/GC/logique/LTL/one_step_leads_to.con
+cic:/Marseille/GC/logique/LTL/run.con
+cic:/Marseille/GC/logique/LTL/safe_and.con
+cic:/Marseille/GC/logique/LTL/safe_and_state.con
+cic:/Marseille/GC/logique/LTL/safe.con
+cic:/Marseille/GC/logique/LTL/safeP_safeQ.con
+cic:/Marseille/GC/logique/LTL/safeP_safeQ_stream.con
+cic:/Marseille/GC/logique/LTL/safety.con
+cic:/Marseille/GC/logique/LTL/state2stream_formula.con
+cic:/Marseille/GC/logique/LTL/state_formula.con
+cic:/Marseille/GC/logique/LTL/step.ind
+cic:/Marseille/GC/logique/LTL/step_ind.con
+cic:/Marseille/GC/logique/LTL/stream_formula.con
+cic:/Marseille/GC/logique/LTL/stream.ind
+cic:/Marseille/GC/logique/LTL/strong_fairstr.con
+cic:/Marseille/GC/logique/LTL/strong_fairstr_implies_fairstr.con
+cic:/Marseille/GC/logique/LTL/tl_str.con
+cic:/Marseille/GC/logique/LTL/trace.con
+cic:/Marseille/GC/logique/LTL/unless.ind
+cic:/Marseille/GC/logique/LTL/until_eventually.con
+cic:/Marseille/GC/logique/LTL/until_implies_until.con
+cic:/Marseille/GC/logique/LTL/until_implies_until_state.con
+cic:/Marseille/GC/logique/LTL/until_implies_until_stream.con
+cic:/Marseille/GC/logique/LTL/until.ind
+cic:/Marseille/GC/logique/LTL/until_ind.con
+cic:/Marseille/GC/logique/LTL/until_or.con
+cic:/Marseille/GC/logique/LTL/until_trans.con
+cic:/Marseille/GC/logique/well_founded/wf_leadsto.con
+cic:/Marseille/GC/logique/well_founded/wf_leadsto_rule.con
+cic:/Marseille/GC/mesure/black_card/add_black.con
+cic:/Marseille/GC/mesure/black_card/alloc_black.con
+cic:/Marseille/GC/mesure/black_card/ex_add_black.con
+cic:/Marseille/GC/mesure/black_card/ex_alloc_black.con
+cic:/Marseille/GC/mesure/black_card/ex_gccall_black.con
+cic:/Marseille/GC/mesure/black_card/ex_gcend_black.con
+cic:/Marseille/GC/mesure/black_card/ex_gcfree1_black.con
+cic:/Marseille/GC/mesure/black_card/ex_gcfree_black.con
+cic:/Marseille/GC/mesure/black_card/ex_gcstop_black.con
+cic:/Marseille/GC/mesure/black_card/ex_init_black.con
+cic:/Marseille/GC/mesure/black_card/ex_marknode_black.con
+cic:/Marseille/GC/mesure/black_card/ex_remove_black.con
+cic:/Marseille/GC/mesure/black_card/gcend_black.con
+cic:/Marseille/GC/mesure/black_card/gcfree1_black.con
+cic:/Marseille/GC/mesure/black_card/gcfree_black.con
+cic:/Marseille/GC/mesure/black_card/gcstop_black.con
+cic:/Marseille/GC/mesure/black_card/greynode_black.con
+cic:/Marseille/GC/mesure/black_card/init_black.con
+cic:/Marseille/GC/mesure/black_card/initcol_black.con
+cic:/Marseille/GC/mesure/black_card/remove_black.con
+cic:/Marseille/GC/mesure/grey_card/add_grey.con
+cic:/Marseille/GC/mesure/grey_card/alloc_grey.con
+cic:/Marseille/GC/mesure/grey_card/card_grey_marknode.con
+cic:/Marseille/GC/mesure/grey_card/ex_add_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_alloc_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_gccall_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_gcend_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_gcfree1_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_gcfree_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_gcstop_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_init_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_marknode_grey.con
+cic:/Marseille/GC/mesure/grey_card/ex_remove_grey.con
+cic:/Marseille/GC/mesure/grey_card/gcend_grey.con
+cic:/Marseille/GC/mesure/grey_card/gcfree1_grey.con
+cic:/Marseille/GC/mesure/grey_card/gcfree_grey.con
+cic:/Marseille/GC/mesure/grey_card/gcstop_grey.con
+cic:/Marseille/GC/mesure/grey_card/greynode_card_white.con
+cic:/Marseille/GC/mesure/grey_card/initcol_grey.con
+cic:/Marseille/GC/mesure/grey_card/init_grey.con
+cic:/Marseille/GC/mesure/grey_card/remove_grey.con
+cic:/Marseille/GC/mesure/mesure/add_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/add_mesure.con
+cic:/Marseille/GC/mesure/mesure/alloc_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/alloc_mesure.con
+cic:/Marseille/GC/mesure/mesure/gccall_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/gccall_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcend_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcend_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcfree1_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcfree1_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcfree_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcfree_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcstop_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/gcstop_mesure.con
+cic:/Marseille/GC/mesure/mesure/init_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/init_mesure.con
+cic:/Marseille/GC/mesure/mesure/marknode_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/marknode_mesure.con
+cic:/Marseille/GC/mesure/mesure/mesure.ind
+cic:/Marseille/GC/mesure/mesure/mesure_ind.con
+cic:/Marseille/GC/mesure/mesure/remove_ex_mesure.con
+cic:/Marseille/GC/mesure/mesure/remove_mesure.con
+cic:/Marseille/GC/mesure/parameters_card/card_color.con
+cic:/Marseille/GC/mesure/parameters_card/card_sons.ind
+cic:/Marseille/GC/mesure/parameters_card/card_sons_ind.con
+cic:/Marseille/GC/mesure/parameters_card/exist_updated_heap.con
+cic:/Marseille/GC/mesure/parameters_card/grey_white_sons.ind
+cic:/Marseille/GC/mesure/parameters_card/grey_white_sons_ind.con
+cic:/Marseille/GC/mesure/parameters_card/grey_white_sons_rec.con
+cic:/Marseille/GC/mesure/parameters_card/grey_white_sons_rect.con
+cic:/Marseille/GC/mesure/parameters_card/is_true.con
+cic:/Marseille/GC/mesure/parameters_card/is_white.con
+cic:/Marseille/GC/mesure/parameters_card/not_true_and_white.con
+cic:/Marseille/GC/mesure/parameters_card/update_heap.con
+cic:/Marseille/GC/mesure/safe_card/always_card_black.con
+cic:/Marseille/GC/mesure/safe_card/always_card_grey.con
+cic:/Marseille/GC/mesure/safe_card/always_card_white.con
+cic:/Marseille/GC/mesure/safe_card/always_gwb.con
+cic:/Marseille/GC/mesure/safe_card/always_mesure.con
+cic:/Marseille/GC/mesure/safe_card/conj_inv.con
+cic:/Marseille/GC/mesure/safe_card/g_w_b.con
+cic:/Marseille/GC/mesure/safe_card/init_conj_inv.con
+cic:/Marseille/GC/mesure/safe_card/init_inv_conj.con
+cic:/Marseille/GC/mesure/safe_card/init_inv_conj_mes.con
+cic:/Marseille/GC/mesure/safe_card/invariant_conj_inv.con
+cic:/Marseille/GC/mesure/safe_card/invariant_inv_conj.con
+cic:/Marseille/GC/mesure/safe_card/invariant_inv_conj_mes.con
+cic:/Marseille/GC/mesure/safe_card/inv_black_card.con
+cic:/Marseille/GC/mesure/safe_card/inv_conj.con
+cic:/Marseille/GC/mesure/safe_card/inv_conj_mes.con
+cic:/Marseille/GC/mesure/safe_card/safe_card_black.con
+cic:/Marseille/GC/mesure/safe_card/safe_card_grey.con
+cic:/Marseille/GC/mesure/safe_card/safe_card_white.con
+cic:/Marseille/GC/mesure/safe_card/safe_conj_inv.con
+cic:/Marseille/GC/mesure/safe_card/safe_gwb.con
+cic:/Marseille/GC/mesure/safe_card/safe_inv_conj.con
+cic:/Marseille/GC/mesure/safe_card/safe_inv_conj_mes.con
+cic:/Marseille/GC/mesure/safe_card/safe_mesure.con
+cic:/Marseille/GC/mesure/safe_card/step_black_card.con
+cic:/Marseille/GC/mesure/safe_card/step_ex_mesure.con
+cic:/Marseille/GC/mesure/safe_card/step_grey_card.con
+cic:/Marseille/GC/mesure/safe_card/step_mesure.con
+cic:/Marseille/GC/mesure/safe_card/step_white_card.con
+cic:/Marseille/GC/mesure/unicite_mes/measure_unicity.con
+cic:/Marseille/GC/mesure/white_card/add_white.con
+cic:/Marseille/GC/mesure/white_card/alloc_white.con
+cic:/Marseille/GC/mesure/white_card/card_white_marknode.con
+cic:/Marseille/GC/mesure/white_card/ex_add_white.con
+cic:/Marseille/GC/mesure/white_card/ex_alloc_white.con
+cic:/Marseille/GC/mesure/white_card/ex_gccall_white.con
+cic:/Marseille/GC/mesure/white_card/ex_gcend_white.con
+cic:/Marseille/GC/mesure/white_card/ex_gcfree1_white.con
+cic:/Marseille/GC/mesure/white_card/ex_gcfree_white.con
+cic:/Marseille/GC/mesure/white_card/ex_gcstop_white.con
+cic:/Marseille/GC/mesure/white_card/ex_init_white.con
+cic:/Marseille/GC/mesure/white_card/ex_marknode_white.con
+cic:/Marseille/GC/mesure/white_card/ex_remove_white.con
+cic:/Marseille/GC/mesure/white_card/gcend_white.con
+cic:/Marseille/GC/mesure/white_card/gcfree1_white.con
+cic:/Marseille/GC/mesure/white_card/gcfree_white.con
+cic:/Marseille/GC/mesure/white_card/gcstop_white.con
+cic:/Marseille/GC/mesure/white_card/greynode_card_white.con
+cic:/Marseille/GC/mesure/white_card/initcol_white.con
+cic:/Marseille/GC/mesure/white_card/init_white.con
+cic:/Marseille/GC/mesure/white_card/remove_white.con
+cic:/Marseille/GC/reachable/reachable/accessible.con
+cic:/Marseille/GC/reachable/reachable/reachable.ind
+cic:/Marseille/GC/reachable/reachable/reachable_ind.con
+cic:/Marseille/GC/reachable/reachable/reach_acc.con
+cic:/Marseille/GC/reachable/reachable/reach_notacc.con
+cic:/Marseille/GC/reachable/reachable/reach_true_reach.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_addedge.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_alloc.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_gccall.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_gcend.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_gcfree1.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_gcfree.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_gcstop.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_init.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_marknode.con
+cic:/Marseille/GC/safety/accnotfree/acc_imp_notfree_removeedge.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/black_grey_node.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/imp1.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/imp2.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/initcolor_imp_noblack.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_addedge.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_alloc.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_gccall.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_gcend.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_gcfree1.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_gcfree_bis.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_gcfree.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_gcstop.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_init.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_marknode.con
+cic:/Marseille/GC/safety/noedgeblacktowhite/no_edge_black_to_white_removeedge.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_addedge.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_alloc.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_gccall.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_gcend.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_gcfree1.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_gcfree.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_gcstop.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_init.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_marknode.con
+cic:/Marseille/GC/safety/nogreyaccnblackn/nogrey_accn_imp_blackn_removeedge.con
+cic:/Marseille/GC/safety/rtgreyorblack/black_grey_node.con
+cic:/Marseille/GC/safety/rtgreyorblack/free_white_node.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_addedge.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_alloc.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_gccall.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_gcend.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_gcfree1.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_gcfree.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_gcstop.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_init.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_marknode.con
+cic:/Marseille/GC/safety/rtgreyorblack/rt_grey_or_black_removeedge.con
+cic:/Marseille/GC/safety/safety/acc_imp_notfree_step.con
+cic:/Marseille/GC/safety/safety/always_invariant_safety_and.con
+cic:/Marseille/GC/safety/safety/always_inv_safety.con
+cic:/Marseille/GC/safety/safety/always_nogrey_accn_imp_blackn.con
+cic:/Marseille/GC/safety/safety/always_sweep_no_grey.con
+cic:/Marseille/GC/safety/safety/implies_safety_prop.con
+cic:/Marseille/GC/safety/safety/init_invariant_safe.con
+cic:/Marseille/GC/safety/safety/invariant_safe.con
+cic:/Marseille/GC/safety/safety/invariant_safety_and.con
+cic:/Marseille/GC/safety/safety/invariant_safety.con
+cic:/Marseille/GC/safety/safety/inv_invariant_safety.con
+cic:/Marseille/GC/safety/safety/inv_safety_prop.con
+cic:/Marseille/GC/safety/safety/no_edge_black_to_white_inv.con
+cic:/Marseille/GC/safety/safety/no_edge_black_to_white_step.con
+cic:/Marseille/GC/safety/safety/nogrey_accn_imp_blackn_step.con
+cic:/Marseille/GC/safety/safety/rt_grey_or_black_inv.con
+cic:/Marseille/GC/safety/safety/rt_grey_or_black_step.con
+cic:/Marseille/GC/safety/safety/safe_sweep_no_greys.con
+cic:/Marseille/GC/safety/safety/safety_prop.con
+cic:/Marseille/GC/safety/safety/safety_prop_safe.con
+cic:/Marseille/GC/safety/safety/sweep_no_greys_inv.con
+cic:/Marseille/GC/safety/safety/sweep_no_greys_step.con
+cic:/Marseille/GC/safety/sweepnogrey/absurd.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_addedge.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_alloc.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_gccall.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_gcend.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_gcfree1.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_gcfree.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_gcstop.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_init.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_marknode.con
+cic:/Marseille/GC/safety/sweepnogrey/sweep_no_greys_removeedge.con
index 4686922df1afe6a619e2558b01fdc228d1186477..ba226c0d848bcf48fc8b2f9c428d01ef83e4ed90 100644 (file)
@@ -18,14 +18,14 @@ let convert_term uri n_fl t =
  | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp 
  | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
  | NCic.Implicit _ -> assert false
- | NCic.Const (NReference.Ref (_,u,NReference.Ind i)) -> 
+ | NCic.Const (NReference.Ref (_,u,NReference.Ind (_,i))) -> 
      Cic.MutInd (NUri.ouri_of_nuri u,i,[])
  | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) -> 
      Cic.MutConstruct (NUri.ouri_of_nuri u,i,j,[])
  | NCic.Const (NReference.Ref (_,u,NReference.Def))
  | NCic.Const (NReference.Ref (_,u,NReference.Decl)) ->
      Cic.Const (NUri.ouri_of_nuri u,[])
- | NCic.Match (NReference.Ref (_,u,NReference.Ind i),oty,t,pl) ->
+ | NCic.Match (NReference.Ref (_,u,NReference.Ind (_,i)),oty,t,pl) ->
      Cic.MutCase (NUri.ouri_of_nuri u,i, convert_term k oty, convert_term k t,
        List.map (convert_term k) pl)
  | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_))) 
index e867b74934e4c51a52ad1c79a30bc620040d667a..38982d799768183d7353f1d205cfe2236000a699 100644 (file)
@@ -91,7 +91,7 @@ let get_checked_def = function
 ;;
 
 let get_checked_indtys = function
-  | NReference.Ref (_, uri, (NReference.Ind n|NReference.Con (n,_))) ->
+  | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
       (match get_checked_obj uri with
       | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
         inductive,leftno,tys,att,n
index 878740c0c375bcc7a2637d1361b446d6be9618cd..a38ecde4c32051d8d2677b3010ce39ece9ca49af 100644 (file)
@@ -14,7 +14,7 @@ module R = NReference
 let r2s pp_fix_name r = 
   try
     match r with
-    | R.Ref (_,u,R.Ind i) -> 
+    | R.Ref (_,u,R.Ind (_,i)) -> 
         (match NCicLibrary.get_obj u with
         | _,_,_,_, C.Inductive (_,_,itl,_) ->
             let _,name,_,_ = List.nth itl i in name
index 25042b4cdf8b1d6aee7f82145cee50ac4d29a9ca..7e0f483d301adf6773d5bc4e9822a291caa40113 100644 (file)
@@ -111,7 +111,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context =
        if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
     | C.Meta _ -> t
     | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) 
-    | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 ->
+    | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
        C.Rel (k + number_of_types - no)
     | t -> U.map (fun _ k -> k+1) k aux t
   in
@@ -190,8 +190,8 @@ let rec instantiate_parameters params c =
 
 let specialize_inductive_type_constrs ~subst context ty_term =
   match R.whd ~subst context ty_term with
-  | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref)  
-  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty ->
+  | C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref)  
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
       let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
       let left_args,_ = HExtlib.split_nth leftno args in
@@ -249,8 +249,8 @@ let rec weakly_positive ~subst context n nn uri te =
   let dummy = C.Sort (C.Type ~-1) in
   (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy _ = function
-    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+    | C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))))::tl) 
         when NUri.eq uri' uri -> dummy
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
@@ -282,7 +282,7 @@ and strictly_positive ~subst context n nn te =
        strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.for_all (does_not_occur ~subst context n nn) tl
-   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> 
+   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
       let ok = List.length tyl = 1 in
@@ -416,7 +416,7 @@ let rec typeof ~subst ~metasenv context term =
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
-   | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
+   | C.Match (Ref.Ref (_,_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
       let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
       let constructorsno =
@@ -805,13 +805,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
          ) bos
       in
        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
-  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
+  | C.Match (Ref.Ref (_,uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
-        (* TODO: add CoInd to references so that this call is useless *)
-        let isinductive, _, _, _, _ = E.get_checked_indtys ref in
-        if not isinductive then recursor aux k t
-        else
          let ty = typeof ~subst ~metasenv context term in
          let dc_ctx, dcl, start, stop = 
            specialize_and_abstract_constrs ~subst r_uri r_len context ty in
@@ -953,17 +949,17 @@ and is_really_smaller
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
-  | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) 
-  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
-     let isinductive, _, itl, _, _ = E.get_checked_indtys ref in
-     if isinductive then None else (Some (uri,List.length itl))
+  | C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref) 
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref)::_) ->
+     let _, _, itl, _, _ = E.get_checked_indtys ref in
+     Some (uri,List.length itl)
   | C.Prod (n,so,de) ->
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
 
 and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 
   match E.get_checked_obj uri, ref with
-  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind (_,i))  ->
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
       let _,_,_,cl = List.nth tl i in 
index edb69c7bfe4ac2243f7dbb1dd9deedcd85b35683..81a08af4e6bc3037ce24ebc2dac8290c9163af23 100644 (file)
@@ -30,7 +30,7 @@ type spec =
  | Def
  | Fix of int * int (* fixno, recparamno *)
  | CoFix of int
- | Ind of int
+ | Ind of bool * int (* inductive, indtyno *)
  | Con of int * int (* indtyno, constrno *)
 
 type reference = Ref of int * NUri.uri * spec
@@ -91,7 +91,7 @@ fun s ->
         | "def" -> Ref (c (), u, Def)
         | "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j))
         | "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i))
-        | "ind" -> let i = get1 s dot in Ref (c (), u, Ind (i))
+        | "ind" -> let b,i = get2 s dot in Ref (c (), u, Ind (b=1,i))
         | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j))
         | _ -> raise Not_found
       with Not_found -> raise (IllFormedReference (lazy s))
@@ -109,12 +109,12 @@ let string_of_reference (Ref (_,u,indinfo)) =
   | Def -> s2 ^ ".def"
   | Fix (i,j)  -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
   | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
-  | Ind i -> s2 ^ ".ind(" ^ string_of_int i ^ ")"
+  | Ind (b,i)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^")"
   | Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
 ;;
 
 let mk_constructor j = function
-  | Ref (d, u, Ind i) -> 
+  | Ref (d, u, Ind (_,i)) -> 
       reference_of_string (string_of_reference (Ref (d, u, Con (i,j))))
   | _ -> assert false
 ;;
index 1ed27e94dca32e817d221b44f9411a1119235d36..b73239465691af895fde32b484385e5bfb505e2e 100644 (file)
@@ -18,7 +18,7 @@ type spec =
  | Def
  | Fix of int * int (* fixno, recparamno *)
  | CoFix of int
- | Ind of int
+ | Ind of bool * int (* inductive, indtyno *)
  | Con of int * int (* indtyno, constrno *)
 
 type reference = private Ref of int *  NUri.uri * spec
index 77b9a897fed440787aedde1babdce726a89c745b..127d421ccfd06f410fd087418827cbe2e5ea6223 100644 (file)
@@ -569,8 +569,14 @@ let convert_term uri t =
                NCic.Const (Ref.reference_of_ouri curi Ref.Decl)
         | _ -> assert false)
     | Cic.MutInd (curi, tyno, ens) -> 
-       aux_ens k curi octx ctx n_fix uri ens
-        (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind tyno)))
+       let is_inductive =
+        match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+           Cic.InductiveDefinition ([],_,_,_) -> true
+         | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+         | _ -> assert false
+       in
+        aux_ens k curi octx ctx n_fix uri ens
+         (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
     | Cic.MutConstruct (curi, tyno, consno, ens) -> 
        aux_ens k curi octx ctx n_fix uri ens
         (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno))))
@@ -580,7 +586,12 @@ let convert_term uri t =
             aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
          | _ -> assert false)
     | Cic.MutCase (curi, tyno, outty, t, branches) ->
-        let r = Ref.reference_of_ouri curi (Ref.Ind tyno) in
+        let is_inductive =
+         match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+            Cic.InductiveDefinition ([],_,_,_) -> true
+          | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+          | _ -> assert false in
+        let r = Ref.reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
         let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
         let t, fixpoints_t = aux k octx ctx n_fix uri t in
         let branches, fixpoints =