From cf887e708a1050fe39d882fcac5ded83b5341a7a Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 28 Aug 2016 17:45:00 -0400 Subject: Compatibility for 8.5; clear assumptions for an admitted canonicalization proof. --- src/ModularArithmetic/ModularBaseSystemProofs.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3