X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpx_fqus.ma;h=c500be141fa322b2d6d0a1b12e6c1eb89a2d6af0;hb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;hp=06a3573c02fc416194d20663dd20fe8b5bd206a6;hpb=97c627e9d169b5df0308d440a449a6853108f372;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 06a3573c0..c500be141 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) +(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) -include "basic_2/relocation/lifts_tdeq.ma". -include "basic_2/s_computation/fqus_fqup.ma". +include "static_2/relocation/lifts_tdeq.ma". +include "static_2/s_computation/fqus_fqup.ma". include "basic_2/rt_transition/cpx_drops.ma". include "basic_2/rt_transition/cpx_lsubr.ma".