"f" => "aux" to avoid name clashes

[helm.git] / components / library / cicElim.ml

diff --git a/components/library/cicElim.ml b/components/library/cicElim.ml
index fb3c0655cf49c1450449a250c7095fa50094d2e6..c994a9c53865c685bb75ab3ffec85448f0d08db2 100644 (file)
--- a/components/library/cicElim.ml
+++ b/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
@@ -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