From 2e80edafe48a01aa3bb43fa7e32da518822418a0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Tue, 21 Jun 2016 16:58:35 -0700
Subject: Make [bash] tactic easier to debug

Now you don't have to copy/paste the [match goal with ... end].
---
 .mailmap                                           |  1 +
 .../CompleteEdwardsCurveTheorems.v                 | 26 ++++++++++++----------
 2 files changed, 15 insertions(+), 12 deletions(-)

diff --git a/.mailmap b/.mailmap
index fb52e6ce0..c170ccdca 100644
--- a/.mailmap
+++ b/.mailmap
@@ -9,6 +9,7 @@ Jade Philipoom <jadep@mit.edu>                             Jade Philipoom <jadep
 Jade Philipoom <jadep@mit.edu>                             jadep <jade.philipoom@gmail.com>
 Jade Philipoom <jadep@mit.edu>                             jadep <jadep@mit.edu>
 Jason Gross <jgross@mit.edu>                               Jason Gross <jgross@mit.edu>
+Jason Gross <jgross@mit.edu>                               Jason Gross <jagro@google.com>
 Robert Sloan <varomodt@gmail.com>                          Robert Sloan <rsloan@sumologic.com>
 Robert Sloan <varomodt@gmail.com>                          Robert Sloan <varomodt@dhcp-18-189-26-21.dyn.MIT.EDU>
 Robert Sloan <varomodt@gmail.com>                          Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU>
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index b843cd54c..7d728719a 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -109,17 +109,19 @@ Module E.
     Program Definition opp (P:point) : point :=
       exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
 
-    Ltac bash :=
-      repeat match goal with
-             | |- _ => progress intros
-             | [H: _ /\ _ |- _ ] => destruct H
-             | |- _ => progress destruct_points
-             | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in *
-             | |- _ => split
-             | |- Feq _ _ => field_algebra
-             | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto]
-             | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
-             end.
+    Ltac bash_step :=
+      match goal with
+      | |- _ => progress intros
+      | [H: _ /\ _ |- _ ] => destruct H
+      | |- _ => progress destruct_points
+      | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in *
+      | |- _ => split
+      | |- Feq _ _ => field_algebra
+      | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto]
+      | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
+      end.
+
+    Ltac bash := repeat bash_step.
 
     Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. bash. Qed.
     Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed.
@@ -225,4 +227,4 @@ Module E.
              end.
       Qed.
   End Homomorphism.
-End E.
\ No newline at end of file
+End E.
-- 
cgit v1.2.3