From 991c0c66e8ec1763aef5ed3600ed5400cad9d71d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 6 Mar 2020 02:19:54 -0800
Subject: [PATCH] [sledge] Remove unnecessary vocabulary updates

Reviewed By: ngorogiannis

Differential Revision: D20248544

fbshipit-source-id: 84e9c9d89
---
 sledge/src/symbheap/solver.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index ecef5c692..d56cfc422 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -249,7 +249,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
                   {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
                (Sh.rem_seg ssg sub))))
   in
-  goal |> with_ ~us ~com ~min ~xs ~sub ~zs
+  goal |> with_ ~com ~min ~xs ~sub ~zs
 
 (*   [k;    o)
  * ⊢    [l; n)
@@ -420,7 +420,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))
   in
-  goal |> with_ ~us ~com ~min ~xs ~sub ~zs
+  goal |> with_ ~com ~min ~xs ~sub ~zs
 
 (*      [k; o)
  * ⊢ [l;      n)
@@ -462,7 +462,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
                   (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
                   (Sh.rem_seg ssg sub)))))
   in
-  goal |> with_ ~us ~com ~min ~xs ~sub ~zs
+  goal |> with_ ~com ~min ~xs ~sub ~zs
 
 (*      [k;  o)
  * ⊢ [l;   n)