aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-11 19:15:15 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-11 19:15:41 -0400
commit97c72ad6da000682171c819ba712c6c68a09686f (patch)
treefcf95c073028869bfbb88acc03377e5a5fd70b76 /_CoqProject
parente8b12aeec4abea243b7f0be1100a6f33a6ca15ad (diff)
Factor karatsuba through IdfunWithAlt, add test
Currently the refinement is commented out. Also, we drop the proof of equality early (and probably won't use it in the first place); there's no way we can carry around such a proof in reflective-land, so we'll need to add an arithmetical-equality semi-decider to reflective-land that can prove the relevant equalities (or we'll need to leave them over as side-conditions). I expeect this may make things significantly easier on @jadephilipoom.
Diffstat (limited to '_CoqProject')
-rw-r--r--_CoqProject1
1 files changed, 1 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index a62bbd701..068322889 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -207,6 +207,7 @@ src/Specific/ArithmeticSynthesisTest130.v
src/Specific/IntegrationTestDisplayCommon.v
src/Specific/IntegrationTestFreeze.v
src/Specific/IntegrationTestFreezeDisplay.v
+src/Specific/IntegrationTestKaratsubaMul.v
src/Specific/IntegrationTestLadderstep.v
src/Specific/IntegrationTestLadderstep130.v
src/Specific/IntegrationTestLadderstep130Display.v