Removing now useless merging primitives from Evd.

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

1 files changed, 0 insertions, 13 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 932b4cdc1e..50d8b0c8cd 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -237,7 +237,6 @@ module EvarMap = struct
       (fun k v -> assert (v.evar_body == Evar_empty);
         EvarInfoMap.is_defined sigma2 k))
 
-  let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
   let add_constraints (sigma, (us, sm)) cstrs =
     (sigma, (us, Univ.merge_constraints cstrs sm))
 end
@@ -339,14 +338,6 @@ type evar_map =
 let progress_evar_map d1 d2 =
   EvarMap.progress_evar_map d1.evars d2.evars
 
-(* spiwack: tentative. It might very well not be the semantics we want
-     for merging evar_map *)
-let merge d1 d2 = {
-  evars = EvarMap.merge d1.evars d2.evars ;
-  conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ;
-  last_mods = ExistentialSet.union d1.last_mods d2.last_mods ;
-  metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas
-}
 let add d e i = { d with evars=EvarMap.add d.evars e i }
 let remove d e = { d with evars=EvarMap.remove d.evars e }
 let find d e = EvarMap.find d.evars e
@@ -480,10 +471,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
   | Evar (evk2,_) -> fst (evar_source evk2 evd)
   | _ -> Loc.ghost
 
-(* spiwack: should it be replaced by Evd.merge? *)
-let evar_merge evd evars =
-  { evd with evars = EvarMap.merge evd.evars evars.evars }
-
 let evar_list evd c =
   let rec evrec acc c =
     match kind_of_term c with