2 files changed, 12 insertions, 4 deletions
diff --git a/src/Util/Sum.v b/src/Util/Sum.v
index 0bed606c2..d6fa26c2c 100644
--- a/src/Util/Sum.v
+++ b/src/Util/Sum.v
@@ -86,9 +86,13 @@ Ltac induction_path_sum H :=
       end.
 Ltac inversion_sum_step :=
   match goal with
-  | [ H : _ = sum _ _ |- _ ]
+  | [ H : _ = inl _ |- _ ]
     => induction_path_sum H
-  | [ H : sum _ _ = _ |- _ ]
+  | [ H : inl _ = _ |- _ ]
+    => induction_path_sum H
+  | [ H : _ = inr _ |- _ ]
+    => induction_path_sum H
+  | [ H : inr _ = _ |- _ ]
     => induction_path_sum H
   end.
 Ltac inversion_sum := repeat inversion_sum_step.
diff --git a/src/Util/Sumbool.v b/src/Util/Sumbool.v
index a21777605..4008e67f6 100644
--- a/src/Util/Sumbool.v
+++ b/src/Util/Sumbool.v
@@ -57,9 +57,13 @@ Ltac induction_path_sumbool H :=
       end.
 Ltac inversion_sumbool_step :=
   match goal with
-  | [ H : _ = sumbool _ _ |- _ ]
+  | [ H : _ = left _ |- _ ]
     => induction_path_sumbool H
-  | [ H : sumbool _ _ = _ |- _ ]
+  | [ H : left _ = _ |- _ ]
+    => induction_path_sumbool H
+  | [ H : _ = right _ |- _ ]
+    => induction_path_sumbool H
+  | [ H : right _ = _ |- _ ]
     => induction_path_sumbool H
   end.
 Ltac inversion_sumbool := repeat inversion_sumbool_step.