From: Ferruccio Guidi Date: Mon, 23 Oct 2017 17:16:58 +0000 (+0000) Subject: one file missing in previous commit :( X-Git-Tag: make_still_working~427 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=302350938616c335a7b88fb1520b9e66a3cc7994;p=helm.git one file missing in previous commit :( --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma index 6f8e3bc74..e0b7d236c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_3.ma". +include "basic_2/notation/relations/lazyeqsn_3.ma". include "basic_2/syntax/ext2.ma". include "basic_2/relocation/lexs.ma". @@ -23,7 +23,7 @@ definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq cfull. interpretation "ranged equivalence (local environment)" - 'LazyEq f L1 L2 = (lreq f L1 L2). + 'LazyEqSn f L1 L2 = (lreq f L1 L2). (* Basic properties *********************************************************)