]> matita.cs.unibo.it Git - helm.git/commit
update in basic_2 and ground_2
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 16 Apr 2018 19:47:12 +0000 (21:47 +0200)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 16 Apr 2018 19:47:12 +0000 (21:47 +0200)
commit75f395f0febd02de8e0f881d918a8812b1425c8d
treea883855cb2b11233ad1b05d898c7a56a296a10e4
parentd59f344b1e4b377e2f06abd9f8856d686d21b222
update in basic_2 and ground_2

+ some notational changes
+ some renaming
+ some dependences updated
137 files changed:
matita/components/syntax_extensions/.depend
matita/matita/.depend.opt
matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma
matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/ideqsn_3.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_3.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma
matita/matita/contribs/lambdadelta/basic_2/notation/relations/rliftstar_3.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_bind.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight_bind.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lift.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_csx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/scpds_scpds.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_drops.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus_drops.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_lfeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_append.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/fsle.ma
matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma
matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubf.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/lib/star.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rafter_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rat_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcoafter_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rcolength_2.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rintersection_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/rminus_3.ma
matita/matita/contribs/lambdadelta/ground_2/notation/relations/runion_3.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_sor.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_uni.ma
matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl