diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-28 17:45:00 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-31 10:03:57 -0400 |
| commit | cf887e708a1050fe39d882fcac5ded83b5341a7a (patch) | |
| tree | b8bd62465ffd7aa493fec43705a31dc7f474dc19 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | 595c5457b6821403d071088588cf9c2c00cc1d0d (diff) | |
Compatibility for 8.5; clear assumptions for an admitted canonicalization proof.
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index cdcf17e8b..0147a7f60 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -697,7 +697,10 @@ Section CanonicalizationProofs. *) Lemma freeze_canonical : forall u v x y, rep u x -> rep v y -> - (x = y <-> fieldwise Logic.eq (freeze u) (freeze v)). + (x = y <-> fieldwise Logic.eq (freeze u) (freeze v)). + Proof. + clear. + (* TODO: bundle these assumptions so they can be more easily passed to square root proofs? *) Admitted. End CanonicalizationProofs. @@ -714,7 +717,7 @@ Section SquareRootProofs. Proof. cbv [eqb]. intros. rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq). - auto using freeze_canonical. + eauto using freeze_canonical. Qed. Section Sqrt3mod4. |