- test.ma on the disambiguation bug moved to ONAG (just out of the way)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / sstas.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
index ce1aea36e711e7772515a49f2a31f2565680b4a8..de9ca8b0d1d3c22c158352c9f0821aab616cba29 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma
@@ -18,7 +18,7 @@ include "basic_2/static/ssta.ma".
 (* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
 
 (* Note: includes: stass_refl *)
-definition sstas: ∀h. sd h → genv → lenv → relation term ≝
+definition sstas: ∀h. sd h → relation4 genv lenv term term ≝
                   λh,g,G,L. star … (ssta_step h g G L).
 
 interpretation "iterated stratified static type assignment (term)"