From 1bff5420e2a0ad962efa52560c7fbda43ebf1d47 Mon Sep 17 00:00:00 2001 From: Amanda Liu Date: Sun, 6 Feb 2022 12:47:50 -0500 Subject: [PATCH] Update cases tactic to work on N type --- FrapWithoutSets.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v index 2dc0e1b..1c691f3 100644 --- a/FrapWithoutSets.v +++ b/FrapWithoutSets.v @@ -229,6 +229,9 @@ Ltac cases E := ((repeat match type of E with | _ \/ _ => destruct E as [E | E] end) + || (match type of E with + | N => destruct E using indN + end) || (is_var E; destruct E) || match type of E with | {_} + {_} => destruct E