diff options
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r-- | pretyping/evd.ml | 60 |
1 files changed, 0 insertions, 60 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 22e52d138..e1d5c5a98 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -271,12 +271,6 @@ module UNameMap = struct | Some _, _ -> l | _, _ -> r) s t - let diff ext orig = - fold (fun u v acc -> - if mem u orig then acc - else add u v acc) - ext empty - end (* 2nd part used to check consistency on the fly. *) @@ -339,24 +333,6 @@ let union_evar_universe_context ctx ctx' = (* let union_evar_universe_context = *) (* Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *) -let diff_evar_universe_context ctx' ctx = - if ctx == ctx' then empty_evar_universe_context - else - let local = Univ.ContextSet.diff ctx'.uctx_local ctx.uctx_local in - let names = UNameMap.diff ctx'.uctx_names ctx.uctx_names in - { uctx_names = names; - uctx_local = local; - uctx_univ_variables = - Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables; - uctx_univ_algebraic = - Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic; - uctx_universes = ctx.uctx_initial_universes; - uctx_initial_universes = ctx.uctx_initial_universes } - -(* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *) -(* let diff_evar_universe_context = *) -(* Profile.profile2 diff_evar_universe_context_key diff_evar_universe_context;; *) - type 'a in_evar_universe_context = 'a * evar_universe_context let evar_universe_context_set ctx = ctx.uctx_local @@ -996,42 +972,6 @@ let reset_future_goals evd = let restore_future_goals evd gls pgl = { evd with future_goals = gls ; principal_future_goal = pgl } -let meta_diff ext orig = - Metamap.fold (fun m v acc -> - if Metamap.mem m orig then acc - else Metamap.add m v acc) - ext Metamap.empty - -(** ext is supposed to be an extension of odef: - it might have more defined evars, and more - or less undefined ones *) -let diff2 edef eundef odef oundef = - let def = - if odef == edef then EvMap.empty - else - EvMap.fold (fun e v acc -> - if EvMap.mem e odef then acc - else EvMap.add e v acc) - edef EvMap.empty - in - let undef = - if oundef == eundef then EvMap.empty - else - EvMap.fold (fun e v acc -> - if EvMap.mem e oundef then acc - else EvMap.add e v acc) - eundef EvMap.empty - in - (def, undef) - -let diff ext orig = - let defn, undf = diff2 ext.defn_evars ext.undf_evars orig.defn_evars orig.undf_evars in - { ext with - defn_evars = defn; undf_evars = undf; - universes = diff_evar_universe_context ext.universes orig.universes; - metas = meta_diff ext.metas orig.metas - } - (**********************************************************) (* Sort variables *) |