X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fgcp_cr.ma;h=b60a87aef07f9d933e3dc3591a9ac35b49edc340;hb=5832735b721c0bd8567c8f0be761a9136363a2a6;hp=dc9c4498eceb70d7f4830e3f7b60d4bd3eef5de1;hpb=064980eacc2efe70ffee96134d75dfa37506fc36;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
index dc9c4498e..b60a87aef 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
@@ -66,7 +66,7 @@ definition cfun: candidate → candidate → candidate ≝
                  ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
 
 (* the reducibility candidate associated to an atomic arity *)
-let rec acr (RP:candidate) (A:aarity) on A: candidate ≝
+rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝
 match A with
 [ AAtom     ⇒ RP
 | APair B A ⇒ cfun (acr RP B) (acr RP A)