]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/cicElim.ml
fixed a bug in the cleanup ofsedir that was not properly catching #xpointer
[helm.git] / helm / software / components / library / cicElim.ml
index fb3c0655cf49c1450449a250c7095fa50094d2e6..f919d2875e2d7674ff4b4d13facae24a47ffd1c9 100644 (file)
@@ -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