diff options
| -rw-r--r-- | kernel/univ.ml | 5 | ||||
| -rw-r--r-- | pretyping/evd.ml | 21 |
2 files changed, 11 insertions, 15 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index d66ae911d3..dd43e17be5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1882,8 +1882,9 @@ struct let singleton l = of_set (LSet.singleton l) let of_instance i = of_set (Instance.levels i) - let union (univs, cst) (univs', cst') = - LSet.union univs univs', Constraint.union cst cst' + let union (univs, cst as x) (univs', cst' as y) = + if x == y then x + else LSet.union univs univs', Constraint.union cst cst' let append (univs, cst) (univs', cst') = let univs = LSet.fold LSet.add univs univs' in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0fe16f0edd..eb9a8bac6a 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -261,15 +261,16 @@ let instantiate_evar_array info c args = module StringOrd = struct type t = string let compare = String.compare end module UNameMap = struct - - include Map.Make(StringOrd) - - let union s t = + + include Map.Make(StringOrd) + + let union s t = + if s == t then s + else merge (fun k l r -> match l, r with | Some _, _ -> l | _, _ -> r) s t - end (* 2nd part used to check consistency on the fly. *) @@ -307,14 +308,8 @@ let union_evar_universe_context ctx ctx' = if ctx == ctx' then ctx else if is_empty_evar_universe_context ctx' then ctx else - let local = - if ctx.uctx_local == ctx'.uctx_local then ctx.uctx_local - else Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local - in - let names = - if ctx.uctx_names = ctx.uctx_names then ctx.uctx_names - else UNameMap.union ctx.uctx_names ctx'.uctx_names - in + let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in + let names = UNameMap.union ctx.uctx_names ctx'.uctx_names in { uctx_names = names; uctx_local = local; uctx_univ_variables = |