diff options
| author | Pierre-Marie Pédrot | 2019-05-04 19:27:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-04 19:27:40 +0200 |
| commit | 69466c61e5f6315599669fa7255aa5ac37d7b91a (patch) | |
| tree | 95e88ad90441787b768b2931a027c50f54552937 /engine | |
| parent | c05bc427be4455d8fb9341c858ea7e3317ee784e (diff) | |
| parent | 48b86574606b9500864a79ddc6a0a668e1aaf295 (diff) | |
Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions
Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/univMinim.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 6f4f40e2c5..aa14f66df6 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -85,7 +85,7 @@ let union ctx ctx' = let declarenew g = LSet.fold (fun u g -> UGraph.add_universe u false g) newus g in - let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in + let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; uctx_seff_univs = seff; diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 46ff6340b4..fcbf305f9d 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs = (acc, [], LMap.empty, LMap.empty) l in let left = CList.uniquize (List.filter (not_lower lower) left) in - (acc, left, LMap.union newlow lower) + (acc, left, LMap.lunion newlow lower) in let instantiate_lbound lbound = let alg = LSet.mem u algs in |