- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_tls.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
index d461488409aa594d95b33472aed84e9754e3fae1..11a0c9092b8799ca03c5e9db7cc930fac6dc54c8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
@@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_tl.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-let rec tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with
+rec definition tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with
 [ O ⇒ f | S m ⇒ ⫱(tls f m) ].
 
 interpretation "tls (rtmap)" 'DropPreds n f = (tls f n).