From 11e1487d594d633b4db9a24eb4e12b25c755d88a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 18 Nov 2006 17:59:39 +0000
Subject: 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
---
 pretyping/evarutil.ml | 24 ------------------------
 1 file changed, 24 deletions(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 16227d4ba6..469a266974 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 *)
 (**********************)
-- 
cgit v1.2.3