X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=b38512273081907ab6cff86c16cd56f35be304a1;hb=10d3194c1b42dfa72e51000ff2cc217f937b43ac;hp=246751b32785f52b49cad40cff47f7172fffe469;hpb=a09cd4c4c08494249b2af35940c217599130507c;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index 246751b32..b38512273 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -706,20 +706,3 @@ let relations_of_menv m c =
 let sort_metasenv (m : Cic.metasenv) =
   (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
 ;;
-  
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
-  * names as long as they are available, then it fallbacks to name generation
-  * using FreshNamesGenerator module *)
-let namer_of names =
-  let len = List.length names in
-  let count = ref 0 in
-  fun metasenv context name ~typ ->
-    if !count < len then begin
-      let name = match List.nth names !count with
-         | Some s -> Cic.Name s
-	 | None   -> Cic.Anonymous
-      in
-      incr count;
-      name
-    end else
-      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ