From 112e6dced6dad495857a71c7a822f90d7d93d7d9 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 10 Sep 2004 14:27:46 +0000
Subject: Dead code removed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6095 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index ecab905a01..7961a7dc93 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -870,8 +870,6 @@ let rec cic_type_nelist_of_list =
      mkApp ((Lazy.force coq_cons),
       [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |])
 
-let meta_map = ref Evd.Metamap.empty;;
-
 let syntactic_but_representation_of_marked_but hole_relation =
  let rec aux out (rel_out,precise_out,is_reflexive) =
   function
@@ -921,9 +919,7 @@ let syntactic_but_representation_of_marked_but hole_relation =
        else
         let c_is_proper =
          let typ = mkApp (rel_out, [| c ; c |]) in
-         let meta = Clenv.new_meta () in
-          meta_map := Evd.meta_declare meta typ !meta_map ;
-          mkCast (mkMeta meta,typ)
+          mkCast (mkMeta (Clenv.new_meta ()),typ)
         in
          mkApp ((Lazy.force coq_ProperElementToKeep),
           [| hole_relation ; Lazy.force coq_Left2Right; precise_out ;
@@ -959,7 +955,6 @@ let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
        prop_relation precise_prop_relation m ; hyp |])
 
 let relation_rewrite c1 c2 (lft2rgt,cl) gl =
- meta_map := Evd.Metamap.empty ;
  let but = pf_concl gl in
  let (hyp,c1,c2) =
    let cl' =
-- 
cgit v1.2.3