1 files changed, 17 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 8ddfecb5f..cca98c471 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -342,3 +342,20 @@ Ltac revert_last_nondep :=
   end.
 
 Ltac reverse_nondep := repeat revert_last_nondep.
+
+Ltac simplify_repeated_ifs_step :=
+  match goal with
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let x' := match x with
+                 | context x'[b] => let x'' := context x'[true] in x''
+                 end in
+       let G' := context G[if b then x' else y] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let y' := match y with
+                 | context y'[b] => let y'' := context y'[false] in y''
+                 end in
+       let G' := context G[if b then x else y'] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  end.
+Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step.