The fresh_name generator has been moved to ProofEngineHelpers.

[helm.git] / helm / gTopLevel / proofEngineHelpers.ml

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
index d191340ea88b8882a290c100bfc51b0d95f07714..74b6fcdaca1f344032da1afc7df9c393f30f9206 100644 (file)
--- 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]                             *)