From 6c779ae1c2a2f4c798606ce3f7718768387f47a6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 21 Oct 2017 22:23:13 -0400 Subject: Unfold P.bound1 in fenz This will lead to prettier printout --- src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v') diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v index f08605358..dbfc38a7d 100644 --- a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v @@ -304,6 +304,11 @@ Ltac nonzero_preglue op_sig cbv_runtime := | (fun x => ?montgomery_to_F (?meval (?feBW_of_feBW_small _))) => cbv [feBW_of_feBW_small phi meval] end in + lazymatch goal with + | [ |- @sig (?feBW_small -> BoundedWord 1 _ ?bound1) _ ] + => let b1 := (eval vm_compute in bound1) in + change bound1 with b1 + end; apply_lift_sig; intros; eexists_sig_etransitivity; do_red (); [ refine (_ : (if Decidable.dec (_ = 0) then true else false) = _); -- cgit v1.2.3