- extended multiple substitutions now uses bounds in ynat (ie. they

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / cpys.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
index 91f9f35aa7a17dbde34e90b25abf6b50d050c5d7..033034d53bf1893ef098413f73a823ba1d5a5fbf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
@@ -17,7 +17,7 @@ include "basic_2/relocation/cpy.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
 
-definition cpys: nat → nat → relation4 genv lenv term term ≝
+definition cpys: ynat → ynat → relation4 genv lenv term term ≝
                  λd,e,G. LTC … (cpy d e G).
 
 interpretation "context-sensitive extended multiple substritution (term)"