diff options
| author | Maxime Dénès | 2019-04-25 10:32:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-02 12:28:19 +0200 |
| commit | 016ed06128372e7b767efd4d3e1f71df9ca1e3d4 (patch) | |
| tree | 84a2c5c5a68ab9fefce2436e137cd608861b1c70 /engine/uState.ml | |
| parent | ef0ef9f318a0af6542835b71ce7aaced021fff6d (diff) | |
Add union in Map interface
Diffstat (limited to 'engine/uState.ml')
| -rw-r--r-- | engine/uState.ml | 2 |
1 files changed, 1 insertions, 1 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; |