X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=c994a9c53865c685bb75ab3ffec85448f0d08db2;hb=3027a19fa263522f1b736cf97d93f56acc080da6;hp=f919d2875e2d7674ff4b4d13facae24a47ffd1c9;hpb=2aad3e4b468d3e4199712437e7ef82afbbc9553d;p=helm.git

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index f919d2875..c994a9c53 100644
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -357,7 +357,7 @@ let elim_of ~sort uri typeno =
             in
             (* rightno is the decreasing argument, i.e. the argument of
              * inductive type *)
-            Cic.Fix (0, ["f", rightno, final_ty, fixfun])
+            Cic.Fix (0, ["aux", rightno, final_ty, fixfun])
           else
             add_right_lambda dependent leftno (conslen + 1) 1 rightno indty
               mutcase ty