From a1f9d9ee2c662790b43bf56df58121a390efbe7c Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 15 Feb 2019 14:41:47 -0500 Subject: start adapting Montgomery to new glue code --- src/PushButtonSynthesis/Primitives.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/PushButtonSynthesis/Primitives.v') diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index c72b5a50d..24a5592ed 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -135,14 +135,14 @@ Local Notation out_bounds_of_pipeline result Notation FromPipelineToString prefix name result := (Pipeline.FromPipelineToString prefix name result). -Ltac prove_correctness use_curve_good := +Ltac prove_correctness' should_not_clear use_curve_good := let Hres := match goal with H : _ = Success _ |- _ => H end in let H := fresh in pose proof use_curve_good as H; (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) repeat match goal with | [ H' : _ |- _ ] - => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres ] + => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres | should_not_clear H' ] then fail else clear H' end; @@ -163,6 +163,8 @@ Ltac prove_correctness use_curve_good := | progress autorewrite with distr_length in * ] | .. ]. +Ltac prove_correctness use_curve_good := prove_correctness' ltac:(fun _ => fail) use_curve_good. + Module CorrectnessStringification. Module dyn_context. Inductive list := -- cgit v1.2.3