]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/cicElim.ml
"f" => "aux" to avoid name clashes
[helm.git] / components / library / cicElim.ml
index f919d2875e2d7674ff4b4d13facae24a47ffd1c9..c994a9c53865c685bb75ab3ffec85448f0d08db2 100644 (file)
@@ -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