diff options
| author |  jadep <jadep@mit.edu> | 2019-02-15 14:41:47 -0500 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-02-21 11:10:12 -0500 |
| commit | a1f9d9ee2c662790b43bf56df58121a390efbe7c (patch) | |
| tree | 7398e0136b4d0c5b314d9d9943ed9d5d404b8e85 /src/PushButtonSynthesis/Primitives.v | |
| parent | 47c0533d8640af625d6f403a0784edaa6cc26fac (diff) | |
start adapting Montgomery to new glue code
Diffstat (limited to 'src/PushButtonSynthesis/Primitives.v')
| -rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 6 |
1 files changed, 4 insertions, 2 deletions
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 := |