Code mort (duplication de code dans reductionops.ml)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9388 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 24 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 16227d4ba..469a26697 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -125,30 +125,6 @@ let non_instantiated sigma =
 	 ((ev,nf_evar_info sigma evd)::l) else l)
     [] listev
 
-(*************************************)
-(* Metas *)
-
-let meta_value evd mv = 
-  let rec valrec mv =
-    try
-      let b = meta_fvalue evd mv in
-      instance
-        (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
-        b.rebus
-    with Anomaly _ | Not_found -> 
-      mkMeta mv
-  in 
-  valrec mv
-
-let meta_instance env b =
-  let c_sigma =
-    List.map 
-      (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
-  in 
-  instance c_sigma b.rebus
-
-let nf_meta env c = meta_instance env (mk_freelisted c)
-
 (**********************)
 (* Creating new evars *)
 (**********************)