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

2 files changed, 0 insertions, 18 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
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index d3155201de..f29a676c6b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -144,7 +144,6 @@ val undefined_list : evar_map -> (evar * evar_info) list
 val to_list : evar_map -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
-val merge : evar_map -> evar_map -> evar_map
 val define : evar -> constr -> evar_map -> evar_map
 
 val is_evar : evar_map -> evar -> bool
@@ -183,10 +182,6 @@ val evar_declare :
       ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 
-(* spiwack: this function seems to somewhat break the abstraction. 
-   [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
-val evar_merge : evar_map -> evar_map -> evar_map
-
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr