Merge pull request #2 from JasonGross/more-const-commutative

More const commutative
mit-plv · Feb 10, 2022 · 41f9e6a · 41f9e6a
2 parents 1ab7d1d + 9a3c223
commit 41f9e6a
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
@@ -1138,8 +1138,6 @@ Qed.
 Definition consts_commutative :=
   fun e => match e with
     ExprApp (o, args) =>
-    (* note: removing the next line makes tests fail *)
-    if (match o with mul _ => true | _ => false end) then e else
     if commutative o then
     let csts_exprs := List.partition isCst args in
     if associative o
@@ -1155,7 +1153,6 @@ Proof using Type.
   step.
   destruct e; trivial.
   destruct n.
-  destruct (match o with mul _ => true | _ => false end); trivial.
   destruct commutative eqn:?; trivial.
   inversion H; clear H; subst.
   epose proof Permutation_partition l isCst.