X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=22bece0338e08f7a777a11464cd6ca5adcbaaf8e;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;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..22bece033 100644
--- a/helm/software/components/library/cicElim.ml
+++ b/helm/software/components/library/cicElim.ml
@@ -217,7 +217,7 @@ let rec branch (uri, typeno) insource paramsno t fix head args =
       if insource then
         (match args with
         | [arg] -> Cic.Appl (fix :: args)
-        | _ -> Cic.Appl (head :: [Cic.Appl args]))
+        | _ -> Cic.Appl (fix :: [Cic.Appl args]))
       else
         (match args with
         | [] -> head
@@ -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