X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicElim.ml;h=22bece0338e08f7a777a11464cd6ca5adcbaaf8e;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;hp=fb3c0655cf49c1450449a250c7095fa50094d2e6;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/library/cicElim.ml b/helm/software/components/library/cicElim.ml
index fb3c0655c..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
@@ -409,7 +409,8 @@ debug_print (lazy (CicPp.ppterm eliminator_body));
         | Cic.Type _ -> "_rect"
         | _ -> assert false
       in
-      let name = UriManager.name_of_uri uri ^ suffix in
+      (* let name = UriManager.name_of_uri uri ^ suffix in *)
+      let name = name ^ suffix in
       let buri = UriManager.buri_of_uri uri in
       let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
       let obj_attrs = [`Class (`Elim sort); `Generated] in