From 6786da162521427921379f05d064c7e47fc2a825 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Tue, 5 Feb 2019 10:39:11 -0500 Subject: Stop numbering patches MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Keeping patches sequentially numbered produces a messy Git history with many renames for compaction. It’s also redundant with the series file. --- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 29 - debian/patches/0002-Remove-test-4429.patch | 46 - ....v-and-4811.v-due-to-timeout-on-small-pla.patch | 1717 -------------------- debian/patches/0004-5127-fails-on-mips.patch | 30 - .../0005-remove-tests-that-need-coqlib.patch | 633 -------- debian/patches/0006-spelling.patch | 320 ---- debian/patches/0007-avoid-usr-bin-env.patch | 32 - debian/patches/0008-python-scripts-libraries.patch | 20 - debian/patches/0009-skip-dot-pc.patch | 13 - debian/patches/5127-fails-on-mips.patch | 30 + ....v-and-4811.v-due-to-timeout-on-small-pla.patch | 1717 ++++++++++++++++++++ debian/patches/Remove-test-4429.patch | 46 + debian/patches/avoid-usr-bin-env.patch | 32 + debian/patches/python-scripts-libraries.patch | 20 + debian/patches/remove-tests-that-need-coqlib.patch | 633 ++++++++ debian/patches/series | 18 +- debian/patches/skip-dot-pc.patch | 13 + debian/patches/spelling.patch | 320 ++++ ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 29 + 19 files changed, 2849 insertions(+), 2849 deletions(-) delete mode 100644 debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch delete mode 100644 debian/patches/0002-Remove-test-4429.patch delete mode 100644 debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch delete mode 100644 debian/patches/0004-5127-fails-on-mips.patch delete mode 100644 debian/patches/0005-remove-tests-that-need-coqlib.patch delete mode 100644 debian/patches/0006-spelling.patch delete mode 100644 debian/patches/0007-avoid-usr-bin-env.patch delete mode 100644 debian/patches/0008-python-scripts-libraries.patch delete mode 100644 debian/patches/0009-skip-dot-pc.patch create mode 100644 debian/patches/5127-fails-on-mips.patch create mode 100644 debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch create mode 100644 debian/patches/Remove-test-4429.patch create mode 100644 debian/patches/avoid-usr-bin-env.patch create mode 100644 debian/patches/python-scripts-libraries.patch create mode 100644 debian/patches/remove-tests-that-need-coqlib.patch create mode 100644 debian/patches/skip-dot-pc.patch create mode 100644 debian/patches/spelling.patch create mode 100644 debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch diff --git a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch deleted file mode 100644 index 2cf6af5c..00000000 --- a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ /dev/null @@ -1,29 +0,0 @@ -From: Stephane Glondu -Date: Sun, 15 Jan 2012 12:34:19 +0100 -Subject: test-suite/success/Nsatz.v: comment out Ceva - -This lemma uses too much memory for many buildds... ---- - test-suite/success/Nsatz.v | 2 ++ - 1 file changed, 2 insertions(+) - -diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v -index e38affd..040169e 100644 ---- a/test-suite/success/Nsatz.v -+++ b/test-suite/success/Nsatz.v -@@ -462,6 +462,7 @@ idtac "chords". - (*Finished transaction in 4. secs (3.959398u,0.s)*) - Qed. - -+(* - Lemma Ceva: forall A B C D E F M:point, - collinear M A D -> collinear M B E -> collinear M C F -> - collinear B C D -> collinear E A C -> collinear F A B -> -@@ -473,6 +474,7 @@ idtac "Ceva". - Time nsatz. - (*Finished transaction in 105. secs (104.121171u,0.474928s)*) - Qed. -+*) - - Lemma bissectrices: forall A B C M:point, - equaltangente C A M M A B -> diff --git a/debian/patches/0002-Remove-test-4429.patch b/debian/patches/0002-Remove-test-4429.patch deleted file mode 100644 index 9baee306..00000000 --- a/debian/patches/0002-Remove-test-4429.patch +++ /dev/null @@ -1,46 +0,0 @@ -From: Enrico Tassi -Date: Thu, 28 Jan 2016 10:11:08 +0100 -Subject: Remove test 4429 - ---- - test-suite/bugs/closed/4429.v | 31 ------------------------------- - 1 file changed, 31 deletions(-) - delete mode 100644 test-suite/bugs/closed/4429.v - -diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v -deleted file mode 100644 -index bf0e570..0000000 ---- a/test-suite/bugs/closed/4429.v -+++ /dev/null -@@ -1,31 +0,0 @@ --Require Import Arith.Compare_dec. --Require Import Unicode.Utf8. -- --Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := -- match n with -- | O => x -- | S n' => f (my_nat_iter n' f x) -- end. -- --Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := -- match mn with -- | (0, 0) => 0 -- | (0, S n') => S n' -- | (S m', 0) => S m' -- | (S m', S n') => -- match le_gt_dec (S m') (S n') with -- | left _ => f (S m', S n' - S m') -- | right _ => f (S m' - S n', S n') -- end -- end. -- --Axiom max_correct_l : ∀ m n : nat, m <= max m n. --Axiom max_correct_r : ∀ m n : nat, n <= max m n. -- --Hint Resolve max_correct_l max_correct_r : arith. -- --Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). --Proof. -- intros. -- Timeout 3 eauto with arith. --Qed. diff --git a/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch deleted file mode 100644 index 45acd396..00000000 --- a/debian/patches/0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch +++ /dev/null @@ -1,1717 +0,0 @@ -From: Enrico Tassi -Date: Wed, 28 Dec 2016 18:18:34 +0100 -Subject: Remove 3441.v and 4811.v due to timeout on small platforms ---- a/test-suite/bugs/closed/3441.v -+++ /dev/null -@@ -1,23 +0,0 @@ --Axiom f : nat -> nat -> nat. --Fixpoint do_n (n : nat) (k : nat) := -- match n with -- | 0 => k -- | S n' => do_n n' (f k k) -- end. -- --Notation big := (_ = _). --Axiom k : nat. --Goal True. --Timeout 1 let H := fresh "H" in -- let x := constr:(let n := 17 in do_n n = do_n n) in -- let y := (eval lazy in x) in -- pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) --Timeout 1 let H := fresh "H" in -- let x := constr:(let n := 17 in do_n n = do_n n) in -- let y := (eval lazy in x) in -- pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) -- --Timeout 1 Time let H := fresh "H" in -- let x := constr:(let n := 17 in do_n n = do_n n) in -- let y := (eval lazy in x) in -- assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) ---- a/test-suite/bugs/closed/4811.v -+++ /dev/null -@@ -1,1685 +0,0 @@ --(* Test about a slowness of f_equal in 8.5pl1 *) -- --(* Submitted by Jason Gross *) -- --(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) --(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) --(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 -- coqtop version 8.5pl1 (April 2016) *) --Require Coq.ZArith.ZArith. -- --Import Coq.ZArith.ZArith. -- --Axiom F : Z -> Set. --Definition Let_In {A P} (x : A) (f : forall y : A, P y) -- := let y := x in f y. --Local Open Scope Z_scope. --Definition modulus : Z := 2^255 - 19. --Axiom decode : list Z -> F modulus. --Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, -- let Zmul := Z.mul in -- let Zadd := Z.add in -- let Zsub := Z.sub in -- let Zpow_pos := Z.pow_pos in -- @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) -- (@decode -- (@Let_In Z (fun _ : Z => list Z) -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (fun z : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (fun z0 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (fun z1 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) -- (fun z2 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (fun z3 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) -- (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (fun z4 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) -- (fun z5 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (fun z6 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) -- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) -- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) -- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (fun z7 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) -- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) -- (Zmul x1 y8)) (Zmul x0 y9))) -- (fun z8 : Z => -- @Let_In Z (fun _ : Z => list Z) -- (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) -- (Z.land z -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) -- (fun z9 : Z => -- @cons Z -- (Z.land z9 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) -- (Z.land z0 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z1 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z2 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land z3 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z4 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land z5 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z6 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land z7 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land z8 -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@nil Z))))))))))))))))))))))) -- (@decode -- (@cons Z -- (Z.land -- (Zadd -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x9 y2) (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) -- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) -- (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) -- (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) -- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) -- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) -- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) -- (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) -- (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) -- (Zpos (xI (xO (xO (xI xH))))))) -- (Z.land -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Zadd -- (Z.shiftr -- (Zadd -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul -- (Zmul x5 y5) -- (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul x9 y2) -- (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) -- (Zmul x3 y8)) -- (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zmul x2 y0) -- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) -- (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) -- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) -- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) -- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) -- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) -- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) -- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) -- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) -- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) -- (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) -- (Z.land -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) -- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) -- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) -- (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) -- (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) -- (Zmul x6 y5)) (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) -- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) -- (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul (Zmul x9 y1) (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) -- (Zmul x7 y4)) (Zmul x6 y5)) -- (Zmul x5 y6)) (Zmul x4 y7)) -- (Zmul x3 y8)) (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) -- (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) -- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) -- (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) -- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x9 y2) (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) (Zmul x3 y8)) -- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) -- (Zmul x6 y7)) (Zmul x5 y8)) -- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) -- (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) -- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) -- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) -- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul -- (Zmul x5 y5) -- (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul -- (Zmul x3 y7) -- (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul x9 y2) -- (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) -- (Zmul x3 y8)) -- (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zmul x2 y0) -- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y3) -- (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) -- (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) -- (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) -- (Zmul x7 y6)) (Zmul x6 y7)) -- (Zmul x5 y8)) (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) -- (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) -- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) -- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) -- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) -- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) -- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) -- (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) -- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) -- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) -- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) -- (@cons Z -- (Z.land -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd -- (Z.shiftr -- (Zadd (Zmul x0 y0) -- (Zmul -- (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y1) -- (Zpos (xO xH))) -- (Zmul x8 y2)) -- (Zmul -- (Zmul x7 y3) -- (Zpos (xO xH)))) -- (Zmul x6 y4)) -- (Zmul -- (Zmul x5 y5) -- (Zpos (xO xH)))) -- (Zmul x4 y6)) -- (Zmul -- (Zmul x3 y7) -- (Zpos (xO xH)))) -- (Zmul x2 y8)) -- (Zmul -- (Zmul x1 y9) -- (Zpos (xO xH)))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul x9 y2) -- (Zmul x8 y3)) -- (Zmul x7 y4)) -- (Zmul x6 y5)) -- (Zmul x5 y6)) -- (Zmul x4 y7)) -- (Zmul x3 y8)) -- (Zmul x2 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zmul x2 y0) -- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) -- (Zmul x0 y2)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zmul -- (Zmul x9 y3) -- (Zpos (xO xH))) -- (Zmul x8 y4)) -- (Zmul -- (Zmul x7 y5) -- (Zpos (xO xH)))) -- (Zmul x6 y6)) -- (Zmul -- (Zmul x5 y7) -- (Zpos (xO xH)))) -- (Zmul x4 y8)) -- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) -- (Zmul x1 y2)) (Zmul x0 y3)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x9 y4) (Zmul x8 y5)) -- (Zmul x7 y6)) -- (Zmul x6 y7)) -- (Zmul x5 y8)) -- (Zmul x4 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x4 y0) -- (Zmul (Zmul x3 y1) (Zpos (xO xH)))) -- (Zmul x2 y2)) -- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) -- (Zmul x0 y4)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) -- (Zmul x8 y6)) -- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) -- (Zmul x6 y8)) -- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) -- (Zmul x2 y3)) (Zmul x1 y4)) -- (Zmul x0 y5)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) -- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zmul x6 y0) -- (Zmul (Zmul x5 y1) (Zpos (xO xH)))) -- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) -- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) -- (Zmul x0 y6)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) -- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) -- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) -- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) -- (Zmul x1 y6)) (Zmul x0 y7)) -- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) -- (Zpos (xI (xO (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) -- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) -- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) -- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) -- (Zmul x0 y8)) -- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) -- (Zpos (xO (xI (xO (xI xH)))))) -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd -- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) -- (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) -- (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) -- (Zpos -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI -- (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) -- (@nil Z)))))))))))). -- cbv beta zeta. -- intros. -- (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". -- Undo. -- Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) diff --git a/debian/patches/0004-5127-fails-on-mips.patch b/debian/patches/0004-5127-fails-on-mips.patch deleted file mode 100644 index 949c33a7..00000000 --- a/debian/patches/0004-5127-fails-on-mips.patch +++ /dev/null @@ -1,30 +0,0 @@ -From: Enrico Tassi -Date: Thu, 29 Dec 2016 08:56:45 +0100 -Subject: 5127 fails on mips - ---- - test-suite/bugs/closed/5127.v | 15 --------------- - 1 file changed, 15 deletions(-) - delete mode 100644 test-suite/bugs/closed/5127.v - -diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v -deleted file mode 100644 -index 831e8fb..0000000 ---- a/test-suite/bugs/closed/5127.v -+++ /dev/null -@@ -1,15 +0,0 @@ --Fixpoint arrow (n: nat) := -- match n with -- | S n => bool -> arrow n -- | O => bool -- end. -- --Fixpoint apply (n : nat) : arrow n -> bool := -- match n return arrow n -> bool with -- | S n => fun f => apply _ (f true) -- | O => fun x => x -- end. -- --Axiom f : arrow 10000. --Definition v : bool := Eval compute in apply _ f. --Definition w : bool := Eval vm_compute in v. diff --git a/debian/patches/0005-remove-tests-that-need-coqlib.patch b/debian/patches/0005-remove-tests-that-need-coqlib.patch deleted file mode 100644 index 48cd1b96..00000000 --- a/debian/patches/0005-remove-tests-that-need-coqlib.patch +++ /dev/null @@ -1,633 +0,0 @@ -From: Benjamin Barenblat -Subject: Disable tests which require -coqlib to be set -Bug: https://github.com/coq/coq/issues/5975 -Forwarded: not-needed - -A number of tests (mostly for coq_makefile) assume that Coq is -installed when the test runs. This isn't true in an sbuild environment, -though, so disable those tests. ---- a/test-suite/misc/printers.sh -+++ /dev/null -@@ -1,3 +0,0 @@ --printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" --if [ $? = 0 ]; then exit 1; else exit 0; fi -- ---- a/test-suite/coq-makefile/arg/run.sh -+++ /dev/null -@@ -1,7 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make ---- a/test-suite/coq-makefile/compat-subdirs/run.sh -+++ /dev/null -@@ -1,8 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --exec test -f "subdir/done" ---- a/test-suite/coq-makefile/coqdoc1/run.sh -+++ /dev/null -@@ -1,51 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --make html mlihtml --make install DSTROOT="$PWD/tmp" --make install-doc DSTROOT="$PWD/tmp" --#make debug --(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired <> src/test_aux.ml --export OCAMLPATH=$OCAMLPATH:$PWD/findlib --if which cygpath 2>/dev/null; then -- # the only way I found to pass OCAMLPATH on win is to have it contain -- # only one entry -- export OCAMLPATH=`cygpath -w $PWD/findlib` --fi --make -C findlib/foo clean --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --cat Makefile.local --make -C findlib/foo --make --make byte ---- a/test-suite/coq-makefile/latex1/run.sh -+++ /dev/null -@@ -1,13 +0,0 @@ --#!/usr/bin/env bash -- --if which pdflatex; then -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --exec make all.pdf -- --fi --exit 0 # test skipped ---- a/test-suite/coq-makefile/merlin1/run.sh -+++ /dev/null -@@ -1,13 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make .merlin --cat > desired < actual --exec diff -u desired actual ---- a/test-suite/coq-makefile/mlpack1/run.sh -+++ /dev/null -@@ -1,23 +0,0 @@ --#!/usr/bin/env bash -- --. ../template/init.sh -- --coq_makefile -f _CoqProject -o Makefile --cat Makefile.conf --make --make html mlihtml --make install DSTROOT="$PWD/tmp" --#make debug --(cd `find tmp -name user-contrib` && find .) | sort > actual --sort > desired < actual --sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort > desired < actual --sort > desired < actual --sort > desired < actual --sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual --sort -u > desired < ${file}${ext}.processed -- done --done --for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do -- echo "cat $file" -- cat "$file" -- echo -- diff -u $file.desired.processed $file.processed || exit $? --done -- --cd ../per-file-before --coq_makefile -f _CoqProject -o Makefile --make cleanall --make all TIMING=before -j2 || exit $? -- --cd ../per-file-after --coq_makefile -f _CoqProject -o Makefile --make cleanall --make all TIMING=after -j2 || exit $? -- --find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' --make all.timing.diff -j2 || exit $? --echo "cat A.v.before-timing" --cat A.v.before-timing --echo --echo "cat A.v.after-timing" --cat A.v.after-timing --echo --echo "cat A.v.timing.diff" --cat A.v.timing.diff --echo -- --for ext in "" .desired; do -- for file in A.v.timing.diff; do -- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed -- done --done --for file in A.v.timing.diff; do -- diff -u $file.desired.processed $file.processed || exit $? --done -- --exit 0 diff --git a/debian/patches/0006-spelling.patch b/debian/patches/0006-spelling.patch deleted file mode 100644 index 149d11b4..00000000 --- a/debian/patches/0006-spelling.patch +++ /dev/null @@ -1,320 +0,0 @@ -From: Benjamin Barenblat -Subject: Correct some spelling errors -Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca -Reviewed-by: Benjamin Barenblat - -Lintian found some spelling errors in the Debian packaging for coq. Fix -them most places they appear in the current source. (Don't change -documentation anchor names, as that would invalidate external -deeplinks.) - -This also fixes a bug in coqdoc: prior to this commit, coqdoc would -highlight `instanciate` but not `instantiate`. ---- a/ide/nanoPG.ml -+++ b/ide/nanoPG.ml -@@ -189,7 +189,7 @@ - run "Edit" "Cut"; - { s with kill = Some(txt,false); sel = false } - else s)); -- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ -> -+ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> - let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in - let k = - if i#ends_line then begin ---- a/kernel/clambda.ml -+++ b/kernel/clambda.ml -@@ -767,7 +767,7 @@ - and such, which can't be done at this time. - for instance, for int31: if one of the digit is - not closed, it's not impossible that the number -- gets fully instanciated at run-time, thus to ensure -+ gets fully instantiated at run-time, thus to ensure - uniqueness of the representation in the vm - it is necessary to try and build a caml integer - during the execution *) ---- a/lib/future.ml -+++ b/lib/future.ml -@@ -49,7 +49,7 @@ - module UUIDMap = Map.Make(UUID) - module UUIDSet = Set.Make(UUID) - --type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] -+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] - - (* Val is not necessarily a final state, so the - computation restarts from the state stocked into Val *) -@@ -103,7 +103,7 @@ - let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn - - let create_delegate ?(blocking=true) ~name fix_exn = -- let assignement signal ck = fun v -> -+ let assignment signal ck = fun v -> - let _, _, fix_exn, c = get ck in - assert (match !c with Delegated _ -> true | _ -> false); - begin match v with -@@ -118,7 +118,7 @@ - (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), - (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in - let ck = create ~name fix_exn (Delegated wait) in -- ck, assignement signal ck -+ ck, assignment signal ck - - (* TODO: get rid of try/catch to be stackless *) - let rec compute ck : 'a value = ---- a/lib/future.mli -+++ b/lib/future.mli -@@ -70,10 +70,10 @@ - (* Run remotely, returns the function to assign. - If not blocking (the default) it raises NotReady if forced before the - delegate assigns it. *) --type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] -+type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] - val create_delegate : - ?blocking:bool -> name:string -> -- fix_exn -> 'a computation * ('a assignement -> unit) -+ fix_exn -> 'a computation * ('a assignment -> unit) - - (* Given a computation that is_exn, replace it by another one *) - val replace : 'a computation -> 'a computation -> unit ---- a/plugins/funind/functional_principles_proofs.ml -+++ b/plugins/funind/functional_principles_proofs.ml -@@ -638,11 +638,11 @@ - (* observe (str "using snd tac since : " ++ CErrors.print e); *) - tac2 g - --let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = -+let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = - let args = Array.of_list (List.map mkVar args_id) in -- let instanciate_one_hyp hid = -+ let instantiate_one_hyp hid = - my_orelse -- ( (* we instanciate the hyp if possible *) -+ ( (* we instantiate the hyp if possible *) - fun g -> - let prov_hid = pf_get_new_id hid g in - let c = mkApp(mkVar hid,args) in -@@ -678,7 +678,7 @@ - tclTHENLIST - [ - tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; -- tclMAP instanciate_one_hyp hyps; -+ tclMAP instantiate_one_hyp hyps; - (fun g -> - let all_g_hyps_id = - List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty -@@ -722,11 +722,11 @@ - tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); - (fun g' -> - let g'_nb_prod = nb_prod (project g') (pf_concl g') in -- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in -+ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in - observe_tac "treat_new_case" - (treat_new_case - ptes_infos -- nb_instanciate_partial -+ nb_instantiate_partial - (build_proof do_finalize) - t - dyn_infos) -@@ -760,7 +760,7 @@ - nb_rec_hyps = List.length new_hyps - } - in --(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' -+(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' - (* build_proof do_finalize new_infos g' *) - ) g - | _ -> -@@ -1118,7 +1118,7 @@ - in - (full_params, (* real params *) - princ_params, (* the params of the principle which are not params of the function *) -- substl (* function instanciated with real params *) -+ substl (* function instantiated with real params *) - (List.map var_of_decl full_params) - f_body - ) -@@ -1128,7 +1128,7 @@ - let f_body = compose_lam f_ctxt_other f_body in - (princ_info.params, (* real params *) - [],(* all params are full params *) -- substl (* function instanciated with real params *) -+ substl (* function instantiated with real params *) - (List.map var_of_decl princ_info.params) - f_body - ) -@@ -1319,7 +1319,7 @@ - (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) - - (* ); *) -- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac -+ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac - (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id)) - ] -@@ -1369,7 +1369,7 @@ - do_prove - dyn_infos - in -- instanciate_hyps_with_args prove_tac -+ instantiate_hyps_with_args prove_tac - (List.rev_map id_of_decl princ_info.branches) - (List.rev args_id) - ] -@@ -1726,8 +1726,8 @@ - ptes_info - (body_info rec_hyps) - in -- (* observe_tac "instanciate_hyps_with_args" *) -- (instanciate_hyps_with_args -+ (* observe_tac "instantiate_hyps_with_args" *) -+ (instantiate_hyps_with_args - make_proof - (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) - (List.rev args_ids) ---- a/plugins/funind/recdef.ml -+++ b/plugins/funind/recdef.ml -@@ -1318,7 +1318,7 @@ - | None -> - try add_suffix current_proof_name "_subproof" - with e when CErrors.noncritical e -> -- anomaly (Pp.str "open_new_goal with an unamed theorem.") -+ anomaly (Pp.str "open_new_goal with an unnamed theorem.") - in - let na = next_global_ident_away name Id.Set.empty in - if Termops.occur_existential sigma gls_type then ---- a/plugins/omega/PreOmega.v -+++ b/plugins/omega/PreOmega.v -@@ -181,7 +181,7 @@ - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t in H - | _ => rewrite (Nat2Z.inj_succ a) in H -- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), -+ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in this one hypothesis *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H - end -@@ -192,7 +192,7 @@ - let t := eval compute in (Z.of_nat (S a)) in - change (Z.of_nat (S a)) with t - | _ => rewrite (Nat2Z.inj_succ a) -- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), -+ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), - hide [Z.of_nat (S a)] in the goal *) - change (Z.of_nat (S a)) with (Z_of_nat' (S a)) - end ---- a/plugins/omega/omega.ml -+++ b/plugins/omega/omega.ml -@@ -178,7 +178,7 @@ - | DIVIDE_AND_APPROX (e1,e2,k,d) -> - Printf.printf - "Inequation E%d is divided by %s and the constant coefficient is \ -- rounded by substracting %s.\n" e1.id (sbi k) (sbi d) -+ rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) - | NOT_EXACT_DIVIDE (e,k) -> - Printf.printf - "Constant in equation E%d is not divisible by the pgcd \ ---- a/stm/stm.ml -+++ b/stm/stm.ml -@@ -1343,7 +1343,7 @@ - t_stop : Stateid.t; - t_drop : bool; - t_states : competence; -- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; -+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; - t_loc : Loc.t option; - t_uuid : Future.UUID.t; - t_name : string } -@@ -1381,7 +1381,7 @@ - t_stop : Stateid.t; - t_drop : bool; - t_states : competence; -- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; -+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; - t_loc : Loc.t option; - t_uuid : Future.UUID.t; - t_name : string } -@@ -1819,7 +1819,7 @@ - type task = { - t_state : Stateid.t; - t_state_fb : Stateid.t; -- t_assign : output Future.assignement -> unit; -+ t_assign : output Future.assignment -> unit; - t_ast : int * aast; - t_goal : Goal.goal; - t_kill : unit -> unit; -@@ -1836,7 +1836,7 @@ - type task = { - t_state : Stateid.t; - t_state_fb : Stateid.t; -- t_assign : output Future.assignement -> unit; -+ t_assign : output Future.assignment -> unit; - t_ast : int * aast; - t_goal : Goal.goal; - t_kill : unit -> unit; ---- a/test-suite/success/univers.v -+++ b/test-suite/success/univers.v -@@ -60,7 +60,7 @@ - - Record U : Type := { A:=Type; a:A }. - --(** Check assignement of sorts to inductives and records. *) -+(** Check assignment of sorts to inductives and records. *) - - Variable sh : list nat. - ---- a/tools/coq_makefile.ml -+++ b/tools/coq_makefile.ml -@@ -59,7 +59,7 @@ - \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ - \n as a dependencies of an already defined target \"foo\".\ - \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ --\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ -+\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ - \n starting from \"physicalpath\". The logical path associated to the\ - \n physical path is \"logicalpath\".\ - \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ ---- a/tools/coqdoc/output.ml -+++ b/tools/coqdoc/output.ml -@@ -76,7 +76,7 @@ - [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; - "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; - "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; -- "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; -+ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; - "quote"; "eexact"; "autorewrite"; - "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; - "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; ---- a/tools/coqworkmgr.ml -+++ b/tools/coqworkmgr.ml -@@ -169,7 +169,7 @@ - "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; - "-d",Arg.Set debug, "do not detach (debug)"] in - let usage = -- "Prints on stdout an env variable assignement to be picked up by coq\n"^ -+ "Prints on stdout an env variable assignment to be picked up by coq\n"^ - "instances in order to limit the maximum number of concurrent workers.\n"^ - "The default value is 2.\n"^ - "Usage:" in ---- a/vernac/comProgramFixpoint.ml -+++ b/vernac/comProgramFixpoint.ml -@@ -254,7 +254,7 @@ - interp_recursive ~cofix ~program_mode:true fixl ntns - in - (* Program-specific code *) -- (* Get the interesting evars, those that were not instanciated *) -+ (* Get the interesting evars, those that were not instantiated *) - let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in - (* Solve remaining evars *) - let evd = nf_evar_map_undefined evd in ---- a/vernac/obligations.ml -+++ b/vernac/obligations.ml -@@ -338,7 +338,7 @@ - let _ = - declare_bool_option - { optdepr = false; -- optname = "Hidding of Program obligations"; -+ optname = "Hiding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } diff --git a/debian/patches/0007-avoid-usr-bin-env.patch b/debian/patches/0007-avoid-usr-bin-env.patch deleted file mode 100644 index 132ed7aa..00000000 --- a/debian/patches/0007-avoid-usr-bin-env.patch +++ /dev/null @@ -1,32 +0,0 @@ -From: Benjamin Barenblat -Subject: Avoid invoking /usr/bin/env -Forwarded: not-needed - -Per Debian Python policy [1], use `/usr/bin/python3` rather than -`/usr/bin/env python` to refer to the system Python (3) interpreter. - -[1] https://www.debian.org/doc/packaging-manuals/python-policy/python.html#interpreter_loc ---- a/tools/make-both-single-timing-files.py -+++ b/tools/make-both-single-timing-files.py -@@ -1,4 +1,4 @@ --#!/usr/bin/env python -+#!/usr/bin/python3 - import sys - from TimeFileMaker import * - ---- a/tools/make-both-time-files.py -+++ b/tools/make-both-time-files.py -@@ -1,4 +1,4 @@ --#!/usr/bin/env python -+#!/usr/bin/python3 - import sys - from TimeFileMaker import * - ---- a/tools/make-one-time-file.py -+++ b/tools/make-one-time-file.py -@@ -1,4 +1,4 @@ --#!/usr/bin/env python -+#!/usr/bin/python3 - import sys - from TimeFileMaker import * - diff --git a/debian/patches/0008-python-scripts-libraries.patch b/debian/patches/0008-python-scripts-libraries.patch deleted file mode 100644 index 66a4a9e9..00000000 --- a/debian/patches/0008-python-scripts-libraries.patch +++ /dev/null @@ -1,20 +0,0 @@ -From: Benjamin Barenblat -Subject: Differentiate between Python scripts and libraries -Forwarded: not-needed - -Eliminate the .py extension from executable Python scripts. ---- a/tools/CoqMakefile.in -+++ b/tools/CoqMakefile.in -@@ -91,9 +91,9 @@ - COQMKFILE ?= "$(COQBIN)coq_makefile" - - # Timing scripts --COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" --COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" --COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" -+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file" -+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files" -+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files" - BEFORE ?= - AFTER ?= - diff --git a/debian/patches/0009-skip-dot-pc.patch b/debian/patches/0009-skip-dot-pc.patch deleted file mode 100644 index ce85adf8..00000000 --- a/debian/patches/0009-skip-dot-pc.patch +++ /dev/null @@ -1,13 +0,0 @@ -From: Benjamin Barenblat -Subject: Ignore .pc directory when building -Forwarded: no ---- a/Makefile -+++ b/Makefile -@@ -53,6 +53,7 @@ - -name '.git' -o \ - -name '.bzr' -o \ - -name 'debian' -o \ -+ -name '.pc' -o \ - -name "$${GIT_DIR}" -o \ - -name '_build' -o \ - -name '_build_ci' -o \ diff --git a/debian/patches/5127-fails-on-mips.patch b/debian/patches/5127-fails-on-mips.patch new file mode 100644 index 00000000..949c33a7 --- /dev/null +++ b/debian/patches/5127-fails-on-mips.patch @@ -0,0 +1,30 @@ +From: Enrico Tassi +Date: Thu, 29 Dec 2016 08:56:45 +0100 +Subject: 5127 fails on mips + +--- + test-suite/bugs/closed/5127.v | 15 --------------- + 1 file changed, 15 deletions(-) + delete mode 100644 test-suite/bugs/closed/5127.v + +diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v +deleted file mode 100644 +index 831e8fb..0000000 +--- a/test-suite/bugs/closed/5127.v ++++ /dev/null +@@ -1,15 +0,0 @@ +-Fixpoint arrow (n: nat) := +- match n with +- | S n => bool -> arrow n +- | O => bool +- end. +- +-Fixpoint apply (n : nat) : arrow n -> bool := +- match n return arrow n -> bool with +- | S n => fun f => apply _ (f true) +- | O => fun x => x +- end. +- +-Axiom f : arrow 10000. +-Definition v : bool := Eval compute in apply _ f. +-Definition w : bool := Eval vm_compute in v. diff --git a/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch new file mode 100644 index 00000000..45acd396 --- /dev/null +++ b/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch @@ -0,0 +1,1717 @@ +From: Enrico Tassi +Date: Wed, 28 Dec 2016 18:18:34 +0100 +Subject: Remove 3441.v and 4811.v due to timeout on small platforms +--- a/test-suite/bugs/closed/3441.v ++++ /dev/null +@@ -1,23 +0,0 @@ +-Axiom f : nat -> nat -> nat. +-Fixpoint do_n (n : nat) (k : nat) := +- match n with +- | 0 => k +- | S n' => do_n n' (f k k) +- end. +- +-Notation big := (_ = _). +-Axiom k : nat. +-Goal True. +-Timeout 1 let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) +-Timeout 1 let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) +- +-Timeout 1 Time let H := fresh "H" in +- let x := constr:(let n := 17 in do_n n = do_n n) in +- let y := (eval lazy in x) in +- assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) +--- a/test-suite/bugs/closed/4811.v ++++ /dev/null +@@ -1,1685 +0,0 @@ +-(* Test about a slowness of f_equal in 8.5pl1 *) +- +-(* Submitted by Jason Gross *) +- +-(* -*- mode: coq; coq-prog-args: ("-R" "src" "Crypto" "-R" "Bedrock" "Bedrock" "-R" "coqprime-8.5/Coqprime" "Coqprime" "-top" "GF255192") -*- *) +-(* File reduced by coq-bug-finder from original input, then from 162 lines to 23 lines, then from 245 lines to 95 lines, then from 198 lines to 101 lines, then from 654 lines to 452 lines, then from 591 lines to 505 lines, then from 1770 lines to 580 lines, then from 2238 lines to 1715 lines, then from 1776 lines to 1738 lines, then from 1750 lines to 1679 lines, then from 1693 lines to 1679 lines *) +-(* coqc version 8.5pl1 (April 2016) compiled on Apr 18 2016 14:48:5 with OCaml 4.02.3 +- coqtop version 8.5pl1 (April 2016) *) +-Require Coq.ZArith.ZArith. +- +-Import Coq.ZArith.ZArith. +- +-Axiom F : Z -> Set. +-Definition Let_In {A P} (x : A) (f : forall y : A, P y) +- := let y := x in f y. +-Local Open Scope Z_scope. +-Definition modulus : Z := 2^255 - 19. +-Axiom decode : list Z -> F modulus. +-Goal forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z, +- let Zmul := Z.mul in +- let Zadd := Z.add in +- let Zsub := Z.sub in +- let Zpow_pos := Z.pow_pos in +- @eq (F (Zsub (Zpow_pos (Zpos (xO xH)) (xI (xI (xI (xI (xI (xI (xI xH)))))))) (Zpos (xI (xI (xO (xO xH))))))) +- (@decode +- (@Let_In Z (fun _ : Z => list Z) +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (fun z : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (fun z0 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z0 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (fun z1 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z1 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (fun z2 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z2 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (fun z3 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z3 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (fun z4 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z4 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (fun z5 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z5 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (fun z6 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z6 (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) +- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (fun z7 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Z.shiftr z7 (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) +- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) +- (Zmul x1 y8)) (Zmul x0 y9))) +- (fun z8 : Z => +- @Let_In Z (fun _ : Z => list Z) +- (Zadd (Zmul (Zpos (xI (xI (xO (xO xH))))) (Z.shiftr z8 (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land z +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (fun z9 : Z => +- @cons Z +- (Z.land z9 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Zadd (Z.shiftr z9 (Zpos (xO (xI (xO (xI xH)))))) +- (Z.land z0 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z1 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z2 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z3 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z4 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z5 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z6 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land z7 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land z8 +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@nil Z))))))))))))))))))))))) +- (@decode +- (@cons Z +- (Z.land +- (Zadd +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) +- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) +- (Zmul x0 y8)) (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) (Zmul x5 y4)) +- (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) +- (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Zadd +- (Z.shiftr +- (Zadd +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) (Zmul x6 y2)) +- (Zmul (Zmul x5 y3) (Zpos (xO xH)))) (Zmul x4 y4)) +- (Zmul (Zmul x3 y5) (Zpos (xO xH)))) (Zmul x2 y6)) +- (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) (Zmul x6 y3)) +- (Zmul x5 y4)) (Zmul x4 y5)) (Zmul x3 y6)) (Zmul x2 y7)) +- (Zmul x1 y8)) (Zmul x0 y9))) (Zpos (xI (xO (xO (xI xH))))))) +- (Z.land +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) +- (Zmul x6 y5)) (Zmul x5 y6)) (Zmul x4 y7)) +- (Zmul x3 y8)) (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y1) (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) (Zmul x7 y4)) +- (Zmul x6 y5)) (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul (Zmul x9 y1) (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul (Zmul x7 y3) (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) (Zmul x6 y5)) +- (Zmul x5 y6)) (Zmul x4 y7)) +- (Zmul x3 y8)) (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul (Zmul x5 y5) (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul (Zmul x3 y7) (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y2) (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) (Zmul x3 y8)) +- (Zmul x2 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zmul x2 y0) (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y3) (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) (Zmul x7 y6)) +- (Zmul x6 y7)) (Zmul x5 y8)) +- (Zmul x4 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) (Zmul x2 y3)) +- (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) (Zmul x6 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) (Zmul x4 y2)) +- (Zmul (Zmul x3 y3) (Zpos (xO xH)))) (Zmul x2 y4)) +- (Zmul (Zmul x1 y5) (Zpos (xO xH)))) (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) (Zmul x4 y3)) +- (Zmul x3 y4)) (Zmul x2 y5)) (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul +- (Zmul x3 y7) +- (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul (Zmul x1 y9) (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y3) +- (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul (Zmul x7 y5) (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul (Zmul x5 y7) (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) (Zmul x1 y2)) +- (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) (Zmul x6 y7)) +- (Zmul x5 y8)) (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x4 y0) (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) +- (Zmul x8 y6)) (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x6 y0) (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) +- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) +- (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) +- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) +- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) +- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))))))))))) +- (@cons Z +- (Z.land +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd +- (Z.shiftr +- (Zadd (Zmul x0 y0) +- (Zmul +- (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y1) +- (Zpos (xO xH))) +- (Zmul x8 y2)) +- (Zmul +- (Zmul x7 y3) +- (Zpos (xO xH)))) +- (Zmul x6 y4)) +- (Zmul +- (Zmul x5 y5) +- (Zpos (xO xH)))) +- (Zmul x4 y6)) +- (Zmul +- (Zmul x3 y7) +- (Zpos (xO xH)))) +- (Zmul x2 y8)) +- (Zmul +- (Zmul x1 y9) +- (Zpos (xO xH)))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd (Zadd (Zmul x1 y0) (Zmul x0 y1)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul x9 y2) +- (Zmul x8 y3)) +- (Zmul x7 y4)) +- (Zmul x6 y5)) +- (Zmul x5 y6)) +- (Zmul x4 y7)) +- (Zmul x3 y8)) +- (Zmul x2 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zmul x2 y0) +- (Zmul (Zmul x1 y1) (Zpos (xO xH)))) +- (Zmul x0 y2)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zmul +- (Zmul x9 y3) +- (Zpos (xO xH))) +- (Zmul x8 y4)) +- (Zmul +- (Zmul x7 y5) +- (Zpos (xO xH)))) +- (Zmul x6 y6)) +- (Zmul +- (Zmul x5 y7) +- (Zpos (xO xH)))) +- (Zmul x4 y8)) +- (Zmul (Zmul x3 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x3 y0) (Zmul x2 y1)) +- (Zmul x1 y2)) (Zmul x0 y3)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x9 y4) (Zmul x8 y5)) +- (Zmul x7 y6)) +- (Zmul x6 y7)) +- (Zmul x5 y8)) +- (Zmul x4 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x4 y0) +- (Zmul (Zmul x3 y1) (Zpos (xO xH)))) +- (Zmul x2 y2)) +- (Zmul (Zmul x1 y3) (Zpos (xO xH)))) +- (Zmul x0 y4)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul (Zmul x9 y5) (Zpos (xO xH))) +- (Zmul x8 y6)) +- (Zmul (Zmul x7 y7) (Zpos (xO xH)))) +- (Zmul x6 y8)) +- (Zmul (Zmul x5 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x5 y0) (Zmul x4 y1)) (Zmul x3 y2)) +- (Zmul x2 y3)) (Zmul x1 y4)) +- (Zmul x0 y5)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zadd (Zmul x9 y6) (Zmul x8 y7)) (Zmul x7 y8)) +- (Zmul x6 y9))))) (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zmul x6 y0) +- (Zmul (Zmul x5 y1) (Zpos (xO xH)))) +- (Zmul x4 y2)) (Zmul (Zmul x3 y3) (Zpos (xO xH)))) +- (Zmul x2 y4)) (Zmul (Zmul x1 y5) (Zpos (xO xH)))) +- (Zmul x0 y6)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) +- (Zadd (Zadd (Zmul (Zmul x9 y7) (Zpos (xO xH))) (Zmul x8 y8)) +- (Zmul (Zmul x7 y9) (Zpos (xO xH))))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x7 y0) (Zmul x6 y1)) (Zmul x5 y2)) +- (Zmul x4 y3)) (Zmul x3 y4)) (Zmul x2 y5)) +- (Zmul x1 y6)) (Zmul x0 y7)) +- (Zmul (Zpos (xI (xI (xO (xO xH))))) (Zadd (Zmul x9 y8) (Zmul x8 y9))))) +- (Zpos (xI (xO (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zmul x8 y0) (Zmul (Zmul x7 y1) (Zpos (xO xH)))) +- (Zmul x6 y2)) (Zmul (Zmul x5 y3) (Zpos (xO xH)))) +- (Zmul x4 y4)) (Zmul (Zmul x3 y5) (Zpos (xO xH)))) +- (Zmul x2 y6)) (Zmul (Zmul x1 y7) (Zpos (xO xH)))) +- (Zmul x0 y8)) +- (Zmul (Zmul (Zmul (Zpos (xI (xI (xO (xO xH))))) x9) y9) (Zpos (xO xH))))) +- (Zpos (xO (xI (xO (xI xH)))))) +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd +- (Zadd (Zadd (Zadd (Zmul x9 y0) (Zmul x8 y1)) (Zmul x7 y2)) +- (Zmul x6 y3)) (Zmul x5 y4)) (Zmul x4 y5)) +- (Zmul x3 y6)) (Zmul x2 y7)) (Zmul x1 y8)) (Zmul x0 y9))) +- (Zpos +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI +- (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))))))))))))) +- (@nil Z)))))))))))). +- cbv beta zeta. +- intros. +- (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early". +- Undo. +- Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *) diff --git a/debian/patches/Remove-test-4429.patch b/debian/patches/Remove-test-4429.patch new file mode 100644 index 00000000..9baee306 --- /dev/null +++ b/debian/patches/Remove-test-4429.patch @@ -0,0 +1,46 @@ +From: Enrico Tassi +Date: Thu, 28 Jan 2016 10:11:08 +0100 +Subject: Remove test 4429 + +--- + test-suite/bugs/closed/4429.v | 31 ------------------------------- + 1 file changed, 31 deletions(-) + delete mode 100644 test-suite/bugs/closed/4429.v + +diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v +deleted file mode 100644 +index bf0e570..0000000 +--- a/test-suite/bugs/closed/4429.v ++++ /dev/null +@@ -1,31 +0,0 @@ +-Require Import Arith.Compare_dec. +-Require Import Unicode.Utf8. +- +-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := +- match n with +- | O => x +- | S n' => f (my_nat_iter n' f x) +- end. +- +-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := +- match mn with +- | (0, 0) => 0 +- | (0, S n') => S n' +- | (S m', 0) => S m' +- | (S m', S n') => +- match le_gt_dec (S m') (S n') with +- | left _ => f (S m', S n' - S m') +- | right _ => f (S m' - S n', S n') +- end +- end. +- +-Axiom max_correct_l : ∀ m n : nat, m <= max m n. +-Axiom max_correct_r : ∀ m n : nat, n <= max m n. +- +-Hint Resolve max_correct_l max_correct_r : arith. +- +-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). +-Proof. +- intros. +- Timeout 3 eauto with arith. +-Qed. diff --git a/debian/patches/avoid-usr-bin-env.patch b/debian/patches/avoid-usr-bin-env.patch new file mode 100644 index 00000000..132ed7aa --- /dev/null +++ b/debian/patches/avoid-usr-bin-env.patch @@ -0,0 +1,32 @@ +From: Benjamin Barenblat +Subject: Avoid invoking /usr/bin/env +Forwarded: not-needed + +Per Debian Python policy [1], use `/usr/bin/python3` rather than +`/usr/bin/env python` to refer to the system Python (3) interpreter. + +[1] https://www.debian.org/doc/packaging-manuals/python-policy/python.html#interpreter_loc +--- a/tools/make-both-single-timing-files.py ++++ b/tools/make-both-single-timing-files.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + +--- a/tools/make-both-time-files.py ++++ b/tools/make-both-time-files.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + +--- a/tools/make-one-time-file.py ++++ b/tools/make-one-time-file.py +@@ -1,4 +1,4 @@ +-#!/usr/bin/env python ++#!/usr/bin/python3 + import sys + from TimeFileMaker import * + diff --git a/debian/patches/python-scripts-libraries.patch b/debian/patches/python-scripts-libraries.patch new file mode 100644 index 00000000..66a4a9e9 --- /dev/null +++ b/debian/patches/python-scripts-libraries.patch @@ -0,0 +1,20 @@ +From: Benjamin Barenblat +Subject: Differentiate between Python scripts and libraries +Forwarded: not-needed + +Eliminate the .py extension from executable Python scripts. +--- a/tools/CoqMakefile.in ++++ b/tools/CoqMakefile.in +@@ -91,9 +91,9 @@ + COQMKFILE ?= "$(COQBIN)coq_makefile" + + # Timing scripts +-COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +-COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +-COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" ++COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file" ++COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files" ++COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files" + BEFORE ?= + AFTER ?= + diff --git a/debian/patches/remove-tests-that-need-coqlib.patch b/debian/patches/remove-tests-that-need-coqlib.patch new file mode 100644 index 00000000..48cd1b96 --- /dev/null +++ b/debian/patches/remove-tests-that-need-coqlib.patch @@ -0,0 +1,633 @@ +From: Benjamin Barenblat +Subject: Disable tests which require -coqlib to be set +Bug: https://github.com/coq/coq/issues/5975 +Forwarded: not-needed + +A number of tests (mostly for coq_makefile) assume that Coq is +installed when the test runs. This isn't true in an sbuild environment, +though, so disable those tests. +--- a/test-suite/misc/printers.sh ++++ /dev/null +@@ -1,3 +0,0 @@ +-printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" +-if [ $? = 0 ]; then exit 1; else exit 0; fi +- +--- a/test-suite/coq-makefile/arg/run.sh ++++ /dev/null +@@ -1,7 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +--- a/test-suite/coq-makefile/compat-subdirs/run.sh ++++ /dev/null +@@ -1,8 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec test -f "subdir/done" +--- a/test-suite/coq-makefile/coqdoc1/run.sh ++++ /dev/null +@@ -1,51 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-make install-doc DSTROOT="$PWD/tmp" +-#make debug +-(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired <> src/test_aux.ml +-export OCAMLPATH=$OCAMLPATH:$PWD/findlib +-if which cygpath 2>/dev/null; then +- # the only way I found to pass OCAMLPATH on win is to have it contain +- # only one entry +- export OCAMLPATH=`cygpath -w $PWD/findlib` +-fi +-make -C findlib/foo clean +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-cat Makefile.local +-make -C findlib/foo +-make +-make byte +--- a/test-suite/coq-makefile/latex1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-if which pdflatex; then +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-exec make all.pdf +- +-fi +-exit 0 # test skipped +--- a/test-suite/coq-makefile/merlin1/run.sh ++++ /dev/null +@@ -1,13 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make .merlin +-cat > desired < actual +-exec diff -u desired actual +--- a/test-suite/coq-makefile/mlpack1/run.sh ++++ /dev/null +@@ -1,23 +0,0 @@ +-#!/usr/bin/env bash +- +-. ../template/init.sh +- +-coq_makefile -f _CoqProject -o Makefile +-cat Makefile.conf +-make +-make html mlihtml +-make install DSTROOT="$PWD/tmp" +-#make debug +-(cd `find tmp -name user-contrib` && find .) | sort > actual +-sort > desired < actual +-sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort > desired < actual +-sort > desired < actual +-sort > desired < actual +-sort > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired </dev/null && find . && popd >/dev/null; done) | sort -u > actual +-sort -u > desired < ${file}${ext}.processed +- done +-done +-for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do +- echo "cat $file" +- cat "$file" +- echo +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-cd ../per-file-before +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=before -j2 || exit $? +- +-cd ../per-file-after +-coq_makefile -f _CoqProject -o Makefile +-make cleanall +-make all TIMING=after -j2 || exit $? +- +-find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +-make all.timing.diff -j2 || exit $? +-echo "cat A.v.before-timing" +-cat A.v.before-timing +-echo +-echo "cat A.v.after-timing" +-cat A.v.after-timing +-echo +-echo "cat A.v.timing.diff" +-cat A.v.timing.diff +-echo +- +-for ext in "" .desired; do +- for file in A.v.timing.diff; do +- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed +- done +-done +-for file in A.v.timing.diff; do +- diff -u $file.desired.processed $file.processed || exit $? +-done +- +-exit 0 diff --git a/debian/patches/series b/debian/patches/series index d2f569c1..2bf642fb 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,9 +1,9 @@ -0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch -0002-Remove-test-4429.patch -0003-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch -0004-5127-fails-on-mips.patch -0005-remove-tests-that-need-coqlib.patch -0006-spelling.patch -0007-avoid-usr-bin-env.patch -0008-python-scripts-libraries.patch -0009-skip-dot-pc.patch +test-suite-success-Nsatz.v-comment-out-Ceva.patch +Remove-test-4429.patch +Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch +5127-fails-on-mips.patch +remove-tests-that-need-coqlib.patch +spelling.patch +avoid-usr-bin-env.patch +python-scripts-libraries.patch +skip-dot-pc.patch diff --git a/debian/patches/skip-dot-pc.patch b/debian/patches/skip-dot-pc.patch new file mode 100644 index 00000000..ce85adf8 --- /dev/null +++ b/debian/patches/skip-dot-pc.patch @@ -0,0 +1,13 @@ +From: Benjamin Barenblat +Subject: Ignore .pc directory when building +Forwarded: no +--- a/Makefile ++++ b/Makefile +@@ -53,6 +53,7 @@ + -name '.git' -o \ + -name '.bzr' -o \ + -name 'debian' -o \ ++ -name '.pc' -o \ + -name "$${GIT_DIR}" -o \ + -name '_build' -o \ + -name '_build_ci' -o \ diff --git a/debian/patches/spelling.patch b/debian/patches/spelling.patch new file mode 100644 index 00000000..149d11b4 --- /dev/null +++ b/debian/patches/spelling.patch @@ -0,0 +1,320 @@ +From: Benjamin Barenblat +Subject: Correct some spelling errors +Origin: backport, https://github.com/coq/coq/commit/06cd051d140a183229cd43f0bbae152d6ad8d6ca +Reviewed-by: Benjamin Barenblat + +Lintian found some spelling errors in the Debian packaging for coq. Fix +them most places they appear in the current source. (Don't change +documentation anchor names, as that would invalidate external +deeplinks.) + +This also fixes a bug in coqdoc: prior to this commit, coqdoc would +highlight `instanciate` but not `instantiate`. +--- a/ide/nanoPG.ml ++++ b/ide/nanoPG.ml +@@ -189,7 +189,7 @@ + run "Edit" "Cut"; + { s with kill = Some(txt,false); sel = false } + else s)); +- mkE _k "k" "Kill untill the end of line" (Edit(fun s b i _ -> ++ mkE _k "k" "Kill until the end of line" (Edit(fun s b i _ -> + let already_killed = match s.kill with Some (k,true) -> k | _ -> "" in + let k = + if i#ends_line then begin +--- a/kernel/clambda.ml ++++ b/kernel/clambda.ml +@@ -767,7 +767,7 @@ + and such, which can't be done at this time. + for instance, for int31: if one of the digit is + not closed, it's not impossible that the number +- gets fully instanciated at run-time, thus to ensure ++ gets fully instantiated at run-time, thus to ensure + uniqueness of the representation in the vm + it is necessary to try and build a caml integer + during the execution *) +--- a/lib/future.ml ++++ b/lib/future.ml +@@ -49,7 +49,7 @@ + module UUIDMap = Map.Make(UUID) + module UUIDSet = Set.Make(UUID) + +-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] ++type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + + (* Val is not necessarily a final state, so the + computation restarts from the state stocked into Val *) +@@ -103,7 +103,7 @@ + let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn + + let create_delegate ?(blocking=true) ~name fix_exn = +- let assignement signal ck = fun v -> ++ let assignment signal ck = fun v -> + let _, _, fix_exn, c = get ck in + assert (match !c with Delegated _ -> true | _ -> false); + begin match v with +@@ -118,7 +118,7 @@ + (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), + (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + let ck = create ~name fix_exn (Delegated wait) in +- ck, assignement signal ck ++ ck, assignment signal ck + + (* TODO: get rid of try/catch to be stackless *) + let rec compute ck : 'a value = +--- a/lib/future.mli ++++ b/lib/future.mli +@@ -70,10 +70,10 @@ + (* Run remotely, returns the function to assign. + If not blocking (the default) it raises NotReady if forced before the + delegate assigns it. *) +-type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] ++type 'a assignment = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] + val create_delegate : + ?blocking:bool -> name:string -> +- fix_exn -> 'a computation * ('a assignement -> unit) ++ fix_exn -> 'a computation * ('a assignment -> unit) + + (* Given a computation that is_exn, replace it by another one *) + val replace : 'a computation -> 'a computation -> unit +--- a/plugins/funind/functional_principles_proofs.ml ++++ b/plugins/funind/functional_principles_proofs.ml +@@ -638,11 +638,11 @@ + (* observe (str "using snd tac since : " ++ CErrors.print e); *) + tac2 g + +-let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = ++let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = + let args = Array.of_list (List.map mkVar args_id) in +- let instanciate_one_hyp hid = ++ let instantiate_one_hyp hid = + my_orelse +- ( (* we instanciate the hyp if possible *) ++ ( (* we instantiate the hyp if possible *) + fun g -> + let prov_hid = pf_get_new_id hid g in + let c = mkApp(mkVar hid,args) in +@@ -678,7 +678,7 @@ + tclTHENLIST + [ + tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; +- tclMAP instanciate_one_hyp hyps; ++ tclMAP instantiate_one_hyp hyps; + (fun g -> + let all_g_hyps_id = + List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty +@@ -722,11 +722,11 @@ + tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); + (fun g' -> + let g'_nb_prod = nb_prod (project g') (pf_concl g') in +- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in ++ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in + observe_tac "treat_new_case" + (treat_new_case + ptes_infos +- nb_instanciate_partial ++ nb_instantiate_partial + (build_proof do_finalize) + t + dyn_infos) +@@ -760,7 +760,7 @@ + nb_rec_hyps = List.length new_hyps + } + in +-(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' ++(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' + (* build_proof do_finalize new_infos g' *) + ) g + | _ -> +@@ -1118,7 +1118,7 @@ + in + (full_params, (* real params *) + princ_params, (* the params of the principle which are not params of the function *) +- substl (* function instanciated with real params *) ++ substl (* function instantiated with real params *) + (List.map var_of_decl full_params) + f_body + ) +@@ -1128,7 +1128,7 @@ + let f_body = compose_lam f_ctxt_other f_body in + (princ_info.params, (* real params *) + [],(* all params are full params *) +- substl (* function instanciated with real params *) ++ substl (* function instantiated with real params *) + (List.map var_of_decl princ_info.params) + f_body + ) +@@ -1319,7 +1319,7 @@ + (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) + + (* ); *) +- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac ++ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id)) + ] +@@ -1369,7 +1369,7 @@ + do_prove + dyn_infos + in +- instanciate_hyps_with_args prove_tac ++ instantiate_hyps_with_args prove_tac + (List.rev_map id_of_decl princ_info.branches) + (List.rev args_id) + ] +@@ -1726,8 +1726,8 @@ + ptes_info + (body_info rec_hyps) + in +- (* observe_tac "instanciate_hyps_with_args" *) +- (instanciate_hyps_with_args ++ (* observe_tac "instantiate_hyps_with_args" *) ++ (instantiate_hyps_with_args + make_proof + (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) + (List.rev args_ids) +--- a/plugins/funind/recdef.ml ++++ b/plugins/funind/recdef.ml +@@ -1318,7 +1318,7 @@ + | None -> + try add_suffix current_proof_name "_subproof" + with e when CErrors.noncritical e -> +- anomaly (Pp.str "open_new_goal with an unamed theorem.") ++ anomaly (Pp.str "open_new_goal with an unnamed theorem.") + in + let na = next_global_ident_away name Id.Set.empty in + if Termops.occur_existential sigma gls_type then +--- a/plugins/omega/PreOmega.v ++++ b/plugins/omega/PreOmega.v +@@ -181,7 +181,7 @@ + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t in H + | _ => rewrite (Nat2Z.inj_succ a) in H +- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), ++ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in this one hypothesis *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H + end +@@ -192,7 +192,7 @@ + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t + | _ => rewrite (Nat2Z.inj_succ a) +- | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), ++ | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in the goal *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) + end +--- a/plugins/omega/omega.ml ++++ b/plugins/omega/omega.ml +@@ -178,7 +178,7 @@ + | DIVIDE_AND_APPROX (e1,e2,k,d) -> + Printf.printf + "Inequation E%d is divided by %s and the constant coefficient is \ +- rounded by substracting %s.\n" e1.id (sbi k) (sbi d) ++ rounded by subtracting %s.\n" e1.id (sbi k) (sbi d) + | NOT_EXACT_DIVIDE (e,k) -> + Printf.printf + "Constant in equation E%d is not divisible by the pgcd \ +--- a/stm/stm.ml ++++ b/stm/stm.ml +@@ -1343,7 +1343,7 @@ + t_stop : Stateid.t; + t_drop : bool; + t_states : competence; +- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; ++ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; + t_loc : Loc.t option; + t_uuid : Future.UUID.t; + t_name : string } +@@ -1381,7 +1381,7 @@ + t_stop : Stateid.t; + t_drop : bool; + t_states : competence; +- t_assign : Proof_global.closed_proof_output Future.assignement -> unit; ++ t_assign : Proof_global.closed_proof_output Future.assignment -> unit; + t_loc : Loc.t option; + t_uuid : Future.UUID.t; + t_name : string } +@@ -1819,7 +1819,7 @@ + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; +- t_assign : output Future.assignement -> unit; ++ t_assign : output Future.assignment -> unit; + t_ast : int * aast; + t_goal : Goal.goal; + t_kill : unit -> unit; +@@ -1836,7 +1836,7 @@ + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; +- t_assign : output Future.assignement -> unit; ++ t_assign : output Future.assignment -> unit; + t_ast : int * aast; + t_goal : Goal.goal; + t_kill : unit -> unit; +--- a/test-suite/success/univers.v ++++ b/test-suite/success/univers.v +@@ -60,7 +60,7 @@ + + Record U : Type := { A:=Type; a:A }. + +-(** Check assignement of sorts to inductives and records. *) ++(** Check assignment of sorts to inductives and records. *) + + Variable sh : list nat. + +--- a/tools/coq_makefile.ml ++++ b/tools/coq_makefile.ml +@@ -59,7 +59,7 @@ + \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ + \n as a dependencies of an already defined target \"foo\".\ + \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ +-\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ ++\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ + \n starting from \"physicalpath\". The logical path associated to the\ + \n physical path is \"logicalpath\".\ + \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ +--- a/tools/coqdoc/output.ml ++++ b/tools/coqdoc/output.ml +@@ -76,7 +76,7 @@ + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; + "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; +- "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; ++ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; + "quote"; "eexact"; "autorewrite"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; +--- a/tools/coqworkmgr.ml ++++ b/tools/coqworkmgr.ml +@@ -169,7 +169,7 @@ + "-j",Arg.Set_int max_tokens, "max number of concurrent jobs"; + "-d",Arg.Set debug, "do not detach (debug)"] in + let usage = +- "Prints on stdout an env variable assignement to be picked up by coq\n"^ ++ "Prints on stdout an env variable assignment to be picked up by coq\n"^ + "instances in order to limit the maximum number of concurrent workers.\n"^ + "The default value is 2.\n"^ + "Usage:" in +--- a/vernac/comProgramFixpoint.ml ++++ b/vernac/comProgramFixpoint.ml +@@ -254,7 +254,7 @@ + interp_recursive ~cofix ~program_mode:true fixl ntns + in + (* Program-specific code *) +- (* Get the interesting evars, those that were not instanciated *) ++ (* Get the interesting evars, those that were not instantiated *) + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in + (* Solve remaining evars *) + let evd = nf_evar_map_undefined evd in +--- a/vernac/obligations.ml ++++ b/vernac/obligations.ml +@@ -338,7 +338,7 @@ + let _ = + declare_bool_option + { optdepr = false; +- optname = "Hidding of Program obligations"; ++ optname = "Hiding of Program obligations"; + optkey = ["Hide";"Obligations"]; + optread = get_hide_obligations; + optwrite = set_hide_obligations; } diff --git a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch new file mode 100644 index 00000000..2cf6af5c --- /dev/null +++ b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -0,0 +1,29 @@ +From: Stephane Glondu +Date: Sun, 15 Jan 2012 12:34:19 +0100 +Subject: test-suite/success/Nsatz.v: comment out Ceva + +This lemma uses too much memory for many buildds... +--- + test-suite/success/Nsatz.v | 2 ++ + 1 file changed, 2 insertions(+) + +diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v +index e38affd..040169e 100644 +--- a/test-suite/success/Nsatz.v ++++ b/test-suite/success/Nsatz.v +@@ -462,6 +462,7 @@ idtac "chords". + (*Finished transaction in 4. secs (3.959398u,0.s)*) + Qed. + ++(* + Lemma Ceva: forall A B C D E F M:point, + collinear M A D -> collinear M B E -> collinear M C F -> + collinear B C D -> collinear E A C -> collinear F A B -> +@@ -473,6 +474,7 @@ idtac "Ceva". + Time nsatz. + (*Finished transaction in 105. secs (104.121171u,0.474928s)*) + Qed. ++*) + + Lemma bissectrices: forall A B C M:point, + equaltangente C A M M A B -> -- cgit v1.2.3