Removing meta_with_name from Evd.

1 files changed, 0 insertions, 33 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 9c53006c13..12a04fcc22 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1451,39 +1451,6 @@ let meta_reassign mv (v, pb) evd =
 let meta_name evd mv =
   try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
 
-let explain_no_such_bound_variable evd id =
-  let mvl =
-    List.rev (Metamap.fold (fun n clb l ->
-      let na = fst (clb_name clb) in
-      if na != Anonymous then out_name na :: l else l)
-    evd.metas []) in
-  errorlabstrm "Evd.meta_with_name"
-    (str"No such bound variable " ++ pr_id id ++
-     (if mvl == [] then str " (no bound variables at all in the expression)."
-      else
-        (str" (possible name" ++
-         str (if List.length mvl == 1 then " is: " else "s are: ") ++
-         pr_enum pr_id mvl ++ str").")))
-
-let meta_with_name evd id =
-  let na = Name id in
-  let (mvl,mvnodef) =
-    Metamap.fold
-      (fun n clb (l1,l2 as l) ->
-        let (na',def) = clb_name clb in
-        if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
-        else l)
-      evd.metas ([],[]) in
-  match mvnodef, mvl with
-    | _,[]  ->
-      explain_no_such_bound_variable evd id
-    | ([n],_|_,[n]) ->
-	n
-    | _  ->
-	errorlabstrm "Evd.meta_with_name"
-          (str "Binder name \"" ++ pr_id id ++
-           strbrk "\" occurs more than once in clause.")
-
 let clear_metas evd = {evd with metas = Metamap.empty}
 
 let meta_merge evd1 evd2 =