diff options
| author | sacerdot | 2004-09-10 14:27:46 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-10 14:27:46 +0000 |
| commit | 112e6dced6dad495857a71c7a822f90d7d93d7d9 (patch) | |
| tree | ad4bac55e6613598147a95265abb6391e4219590 | |
| parent | 6dc7b44c32d6e05bb965ca1e05b3ce191214c0d3 (diff) | |
Dead code removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6095 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 7 |
1 files changed, 1 insertions, 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' = |