More fine-grained util tactic files

Also, add [split_and]

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Util/Tactics/Head.v b/src/Util/Tactics/Head.v
new file mode 100644
index 000000000..fa7a301d6
--- /dev/null
+++ b/src/Util/Tactics/Head.v
@@ -0,0 +1,10 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** find the head of the given expression *)
+Ltac head expr :=
+  match expr with
+  | ?f _ => head f
+  | _ => expr
+  end.
+
+Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.