From 302350938616c335a7b88fb1520b9e66a3cc7994 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 23 Oct 2017 17:16:58 +0000 Subject: [PATCH] one file missing in previous commit :( --- matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 *********************************************************) -- 2.39.2