X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineHelpers.ml;h=74b6fcdaca1f344032da1afc7df9c393f30f9206;hb=370f967a478c116fcc85a81c7953363b4351a2e9;hp=d191340ea88b8882a290c100bfc51b0d95f07714;hpb=4720c6af414c4a834a994fdb404fda2d0c04fc03;p=helm.git

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
index d191340ea..74b6fcdac 100644
--- a/helm/gTopLevel/proofEngineHelpers.ml
+++ b/helm/gTopLevel/proofEngineHelpers.ml
@@ -23,6 +23,17 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(*CSC: generatore di nomi? Chiedere il nome? *)
+let fresh_name =
+ let next_fresh_index = ref 0 in
+  function
+     Cic.Anonymous ->
+      incr next_fresh_index ;
+      "fresh_name" ^ string_of_int !next_fresh_index
+   | Cic.Name name ->
+      incr next_fresh_index ;
+      name ^ string_of_int !next_fresh_index
+
 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 (* where n = List.length [canonical_context]                             *)