From 1b8932d64d40329678dcdb230fb5cc6a95064799 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 14 Dec 2017 11:57:28 -0500 Subject: specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.v --- src/Curves/Montgomery/XZProofs.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'src/Curves') 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 -- cgit v1.2.3