Fix some issues in Ed25519 tactics

- Use replace rather than refine to speed up [Defined] and make the
  tactics easier to read

- Use [apply f_equal] in place of [reflexivity] for unknown presumably
  arcane reasons to satisfy Coq's unifier

- Factor out some tactics into tactic scripts

- Write a lemma to pull functions out of [Let_In]

- Fix autoindentation in emacs by wrapping [Let_In_unRep] in parentheses
  (probably a ProofGeneral regexp gone wrong)

- Write a kludgy tactic to unfold [proj1_sig] only when applied to
  [exist]

(Pair programming with Andres)

0 files changed, 0 insertions, 0 deletions