diff options
| author |  Andres Erbsen <andreser@google.com> | 2017-12-14 11:57:28 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2017-12-22 12:55:33 -0500 |
| commit | 1b8932d64d40329678dcdb230fb5cc6a95064799 (patch) | |
| tree | 815ba7bdf392920b5f33568851ad7e1e10112c5f /src/Curves | |
| parent | d7675322e1ec9509c058c948c237b0aaf6f5ff8c (diff) | |
specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.v
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Montgomery/XZProofs.v | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index 1f5789fc7..fd2a7ee49 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -40,13 +40,14 @@ Module M. match goal with | _ => progress intros | _ => progress autounfold with points_as_coordinates in * - | _ => progress destruct_head' @unit - | _ => progress destruct_head' @bool - | _ => progress destruct_head' @prod - | _ => progress destruct_head' @sig - | _ => progress destruct_head' @sum - | _ => progress destruct_head' @and - | _ => progress destruct_head' @or + | _ => progress destruct_head'_True + | _ => progress destruct_head'_unit + | _ => progress destruct_head'_prod + | _ => progress destruct_head'_sig + | _ => progress destruct_head'_bool + | _ => progress destruct_head'_sum + | _ => progress destruct_head'_and + | _ => progress destruct_head'_or | H: context[dec ?P] |- _ => destruct (dec P) | |- context[dec ?P] => destruct (dec P) | |- ?P => lazymatch type of P with Prop => split end |