diff options
Diffstat (limited to 'test-suite/bugs')
82 files changed, 936 insertions, 1777 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index 3e3a987a7c..e28314cada 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -82,7 +82,7 @@ Notation "F ^op" := (OppositeFunctor F) : functor_scope. Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D') := admit. -Global Class FunctorApplicationInterpretable +Class FunctorApplicationInterpretable {C D} (F : Functor C D) {argsT : Type} (args : argsT) {T : Type} (rtn : T) @@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn} Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}. Global Instance FunctorApplicationDash C D (F : Functor C D) -: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0. +: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}. Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B) -: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100. +: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}. Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope. diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v index 19551dc92e..72bc04e05e 100644 --- a/test-suite/bugs/closed/HoTT_coq_061.v +++ b/test-suite/bugs/closed/HoTT_coq_061.v @@ -96,7 +96,7 @@ Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F' := Build_NaturalTransformation (F o G) (F' o G) (fun c => T (G c)) admit. -Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}. +Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}. Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term. Notation "T 'o' U" diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v index a80d075f69..cd6539b51c 100644 --- a/test-suite/bugs/closed/HoTT_coq_120.v +++ b/test-suite/bugs/closed/HoTT_coq_120.v @@ -89,7 +89,7 @@ Definition set_cat : PreCategory := @Build_PreCategory hSet (fun x y => forall _ : x, y)%core (fun _ _ _ f g x => f (g x))%core. -Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. +Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted. Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT P). Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, diff --git a/test-suite/bugs/closed/bug_2001.v b/test-suite/bugs/closed/bug_2001.v index 652c65706a..31c62b7b36 100644 --- a/test-suite/bugs/closed/bug_2001.v +++ b/test-suite/bugs/closed/bug_2001.v @@ -1,12 +1,10 @@ (* Automatic computing of guard in "Theorem with"; check that guard is not computed when the user explicitly indicated it *) -Unset Automatic Introduction. - Inductive T : Set := | v : T. -Definition f (s:nat) (t:T) : nat. +Definition f : forall (s:nat) (t:T), nat. fix f 2. intros s t. refine diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v index 801c61b132..a321bb324e 100644 --- a/test-suite/bugs/closed/bug_2830.v +++ b/test-suite/bugs/closed/bug_2830.v @@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A). Admitted. Import FunctionalExtensionality. -Instance set_cat : Category Type (fun A B => A -> B) := { + +Instance set_cat : Category Type (fun A B => A -> B). +refine {| id := fun A => fun x => x ; comp c b a f g := fun x => f (g x) ; eqv := fun A B => @skel (A -> B) -}. +|}. intros. compute. symmetry. apply eta_expansion. intros. compute. symmetry. apply eta_expansion. -intros. compute. reflexivity. Defined. +intros. compute. reflexivity. +Defined. (* The [list] type constructor is a Functor. *) diff --git a/test-suite/bugs/closed/bug_3324.v b/test-suite/bugs/closed/bug_3324.v index 45dbb57aa2..dae0d4c024 100644 --- a/test-suite/bugs/closed/bug_3324.v +++ b/test-suite/bugs/closed/bug_3324.v @@ -6,7 +6,7 @@ Module ETassi. Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}. Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). - Global Instance isset_hProp : IsHSet hProp | 0. + Global Instance isset_hProp : IsHSet hProp | 0 := {}. Check (eq_refl _ : setT (default_HSet _ _) = hProp). Check (eq_refl _ : setT _ = hProp). @@ -22,7 +22,7 @@ Module JGross. Definition Unit_hp:hProp:=(hp Unit admit). Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). - Global Instance isset_hProp : IsHSet hProp | 0. + Global Instance isset_hProp : IsHSet hProp | 0 := {}. Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h. Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True. diff --git a/test-suite/bugs/closed/bug_3325.v b/test-suite/bugs/closed/bug_3325.v index 36c065ebe8..835b8a7f33 100644 --- a/test-suite/bugs/closed/bug_3325.v +++ b/test-suite/bugs/closed/bug_3325.v @@ -1,13 +1,13 @@ Typeclasses eauto := debug. Set Printing All. -Axiom SProp : Set. -Axiom sp : SProp. +Axiom sProp : Set. +Axiom sp : sProp. (* If we hardcode valueType := nat, it goes through *) Class StateIs := { valueType : Type; - stateIs : valueType -> SProp + stateIs : valueType -> sProp }. Instance NatStateIs : StateIs := { @@ -17,17 +17,17 @@ Instance NatStateIs : StateIs := { Canonical Structure NatStateIs. Class LogicOps F := { land: F -> F }. -Instance : LogicOps SProp. Admitted. +Instance : LogicOps sProp. Admitted. Instance : LogicOps Prop. Admitted. Parameter (n : nat). (* If this is a [Definition], the resolution goes through fine. *) Notation vn := (@stateIs _ n). Definition vn' := (@stateIs _ n). -Definition GOOD : SProp := +Definition GOOD : sProp := @land _ _ vn'. (* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *) -Definition BAD : SProp := +Definition BAD : sProp := @land _ _ vn. diff --git a/test-suite/bugs/closed/bug_3393.v b/test-suite/bugs/closed/bug_3393.v index d2eb61e3e2..b0b573f5d5 100644 --- a/test-suite/bugs/closed/bug_3393.v +++ b/test-suite/bugs/closed/bug_3393.v @@ -109,6 +109,7 @@ Global Instance isisomorphism_compose' `{Funext} `{@IsIsomorphism (C -> D) F F' T} : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation := @isisomorphism_compose (C -> D) _ _ T' _ _ T _. +Arguments isisomorphism_compose' {H C D F' F''} T' {F} T {H0 H1}. Section lemmas. Context `{Funext}. Variable C : PreCategory. diff --git a/test-suite/bugs/closed/bug_3422.v b/test-suite/bugs/closed/bug_3422.v index 460ae8f110..1305104cdb 100644 --- a/test-suite/bugs/closed/bug_3422.v +++ b/test-suite/bugs/closed/bug_3422.v @@ -175,6 +175,7 @@ Global Instance isisomorphism_compose' `{@IsIsomorphism (C -> D) F F' T} : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation := @isisomorphism_compose (C -> D) _ _ T' _ _ T _. +Arguments isisomorphism_compose' {C D F' F''} T' {F} T {H H0}. Section lemmas. Local Open Scope natural_transformation_scope. diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v index 317efb0b32..f00d2fcf09 100644 --- a/test-suite/bugs/closed/bug_3427.v +++ b/test-suite/bugs/closed/bug_3427.v @@ -146,7 +146,7 @@ Section Univalence. := (equiv_path A B)^-1 f. End Univalence. -Local Inductive minus1Trunc (A :Type) : Type := +Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. diff --git a/test-suite/bugs/closed/bug_3441.v b/test-suite/bugs/closed/bug_3441.v deleted file mode 100644 index 52acb996f8..0000000000 --- a/test-suite/bugs/closed/bug_3441.v +++ /dev/null @@ -1,24 +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) *) -Abort. diff --git a/test-suite/bugs/closed/bug_3454.v b/test-suite/bugs/closed/bug_3454.v index e4cd60cb24..0a01adec33 100644 --- a/test-suite/bugs/closed/bug_3454.v +++ b/test-suite/bugs/closed/bug_3454.v @@ -32,14 +32,14 @@ Local Instance isequiv_tgt_compose A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) (@compose A {xy : B * B & fst xy = snd xy} B - (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)). + (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)) := {}. (* Toplevel input, characters 220-223: *) (* Error: Cannot infer this placeholder. *) Local Instance isequiv_tgt_compose' A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) - (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)). + (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)) := {}. (* Toplevel input, characters 221-232: *) (* Error: *) (* In environment *) @@ -52,7 +52,7 @@ Local Instance isequiv_tgt_compose'' A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) - (fun s => s.(projT1)))). + (fun s => s.(projT1)))) := {}. (* Toplevel input, characters 15-241: Error: Cannot infer an internal placeholder of type "Type" in environment: diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v new file mode 100644 index 0000000000..6ff394bca6 --- /dev/null +++ b/test-suite/bugs/closed/bug_3468.v @@ -0,0 +1,29 @@ +(* Checking that unrelated terms requiring some scope do not affect + the interpretation of tactic-in-term. The "Check" was failing with: + The term "Set" has type "Type" while it is expected to have type + "nat". *) + +Notation bar2 a b := (let __ := ltac:(exact I) in (a + b)%type) (only parsing). +Check bar2 (Set + Set) Set. + +(* Taking into account scopes in notations containing tactic-in-term *) + +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Notation "x ~~" := (x) (at level 0, only parsing) : foo_scope. +Notation bar x := (x%foo) (only parsing). +Notation baz x := ltac:(exact x%foo) (only parsing). +Check bar (O ~~). +Check baz (O ~~). (* Was failing *) + +(* This was reported as bug #8706 *) + +Declare Scope my_scope. +Notation "@ a" := a%nat (at level 100, only parsing) : my_scope. +Delimit Scope my_scope with my. + +Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope. +Definition test := (& (@4))%my. + +(* Check inconsistent scopes *) +Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing). diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v index 7b0883f910..47db64a096 100644 --- a/test-suite/bugs/closed/bug_3495.v +++ b/test-suite/bugs/closed/bug_3495.v @@ -1,7 +1,7 @@ Require Import RelationClasses. Axiom R : Prop -> Prop -> Prop. -Declare Instance : Reflexive R. +Declare Instance R_refl : Reflexive R. Class bar := { x : False }. Record foo := { a : Prop ; b : bar }. diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v index 9d37d1a2d0..07b759afb5 100644 --- a/test-suite/bugs/closed/bug_3682.v +++ b/test-suite/bugs/closed/bug_3682.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. Class Foo. Definition bar `{Foo} (x : Set) := Set. -Instance: Foo. +Instance: Foo := {}. Definition bar1 := bar nat. Definition bar2 := bar ltac:(admit). diff --git a/test-suite/bugs/closed/bug_3690.v b/test-suite/bugs/closed/bug_3690.v index fa30132ab5..9273a20e19 100644 --- a/test-suite/bugs/closed/bug_3690.v +++ b/test-suite/bugs/closed/bug_3690.v @@ -41,8 +41,5 @@ Type@{Top.34} -> Type@{Top.37} Top.36 < Top.34 Top.37 < Top.36 *) *) -Fail Check @qux@{Set Set}. -Check @qux@{Type Type Type Type}. -(* [qux] should only need two universes *) -Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *) -Fail Check @qux@{i j}. +Check @qux@{Type Type}. +(* used to have 4 universes *) diff --git a/test-suite/bugs/closed/bug_3956.v b/test-suite/bugs/closed/bug_3956.v index 115284ec02..456fa11bd0 100644 --- a/test-suite/bugs/closed/bug_3956.v +++ b/test-suite/bugs/closed/bug_3956.v @@ -129,13 +129,13 @@ Module Comodality_Theory (F : Comodality). := IdmapM FPM. Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM. Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM. - Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x. + Definition m : forall x, cip_FPM.fhM.m x = cip_FPM.fkM.m x. Proof. intros x. - refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _). + refine (concat (cmpinvM.m_beta (cmpM.m x)) _). apply path_prod@{i i i}; simpl. - - exact (cmpM.FfstM.mM.m_beta@{i j} x). - - exact (cmpM.FsndM.mM.m_beta@{i j} x). + - exact (cmpM.FfstM.mM.m_beta x). + - exact (cmpM.FsndM.mM.m_beta x). Defined. End cip_FPHM. End isequiv_F_prod_cmp_M. diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v index 806ffb771f..67ecc3087f 100644 --- a/test-suite/bugs/closed/bug_4132.v +++ b/test-suite/bugs/closed/bug_4132.v @@ -26,6 +26,6 @@ Qed. Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. omega. (* Pierre L: according to a comment of bug report #4132, - this might have triggered "Failure(occurence 2)" in the past, + this might have triggered "Failure(occurrence 2)" in the past, but I never managed to reproduce that. *) Qed. diff --git a/test-suite/bugs/closed/bug_4157.v b/test-suite/bugs/closed/bug_4157.v new file mode 100644 index 0000000000..a9e96fcdde --- /dev/null +++ b/test-suite/bugs/closed/bug_4157.v @@ -0,0 +1,272 @@ +(** The following proof is due to a bug in `vm_compute` and was found by + Maxime Dénès and Pierre-Marie Pédrot. *) +Inductive t := +| C_0 : nat -> t +| C_1 : nat -> t +| C_2 : nat -> t +| C_3 : nat -> t +| C_4 : nat -> t +| C_5 : nat -> t +| C_6 : nat -> t +| C_7 : nat -> t +| C_8 : nat -> t +| C_9 : nat -> t +| C_10 : nat -> t +| C_11 : nat -> t +| C_12 : nat -> t +| C_13 : nat -> t +| C_14 : nat -> t +| C_15 : nat -> t +| C_16 : nat -> t +| C_17 : nat -> t +| C_18 : nat -> t +| C_19 : nat -> t +| C_20 : nat -> t +| C_21 : nat -> t +| C_22 : nat -> t +| C_23 : nat -> t +| C_24 : nat -> t +| C_25 : nat -> t +| C_26 : nat -> t +| C_27 : nat -> t +| C_28 : nat -> t +| C_29 : nat -> t +| C_30 : nat -> t +| C_31 : nat -> t +| C_32 : nat -> t +| C_33 : nat -> t +| C_34 : nat -> t +| C_35 : nat -> t +| C_36 : nat -> t +| C_37 : nat -> t +| C_38 : nat -> t +| C_39 : nat -> t +| C_40 : nat -> t +| C_41 : nat -> t +| C_42 : nat -> t +| C_43 : nat -> t +| C_44 : nat -> t +| C_45 : nat -> t +| C_46 : nat -> t +| C_47 : nat -> t +| C_48 : nat -> t +| C_49 : nat -> t +| C_50 : nat -> t +| C_51 : nat -> t +| C_52 : nat -> t +| C_53 : nat -> t +| C_54 : nat -> t +| C_55 : nat -> t +| C_56 : nat -> t +| C_57 : nat -> t +| C_58 : nat -> t +| C_59 : nat -> t +| C_60 : nat -> t +| C_61 : nat -> t +| C_62 : nat -> t +| C_63 : nat -> t +| C_64 : nat -> t +| C_65 : nat -> t +| C_66 : nat -> t +| C_67 : nat -> t +| C_68 : nat -> t +| C_69 : nat -> t +| C_70 : nat -> t +| C_71 : nat -> t +| C_72 : nat -> t +| C_73 : nat -> t +| C_74 : nat -> t +| C_75 : nat -> t +| C_76 : nat -> t +| C_77 : nat -> t +| C_78 : nat -> t +| C_79 : nat -> t +| C_80 : nat -> t +| C_81 : nat -> t +| C_82 : nat -> t +| C_83 : nat -> t +| C_84 : nat -> t +| C_85 : nat -> t +| C_86 : nat -> t +| C_87 : nat -> t +| C_88 : nat -> t +| C_89 : nat -> t +| C_90 : nat -> t +| C_91 : nat -> t +| C_92 : nat -> t +| C_93 : nat -> t +| C_94 : nat -> t +| C_95 : nat -> t +| C_96 : nat -> t +| C_97 : nat -> t +| C_98 : nat -> t +| C_99 : nat -> t +| C_100 : nat -> t +| C_101 : nat -> t +| C_102 : nat -> t +| C_103 : nat -> t +| C_104 : nat -> t +| C_105 : nat -> t +| C_106 : nat -> t +| C_107 : nat -> t +| C_108 : nat -> t +| C_109 : nat -> t +| C_110 : nat -> t +| C_111 : nat -> t +| C_112 : nat -> t +| C_113 : nat -> t +| C_114 : nat -> t +| C_115 : nat -> t +| C_116 : nat -> t +| C_117 : nat -> t +| C_118 : nat -> t +| C_119 : nat -> t +| C_120 : nat -> t +| C_121 : nat -> t +| C_122 : nat -> t +| C_123 : nat -> t +| C_124 : nat -> t +| C_125 : nat -> t +| C_126 : nat -> t +| C_127 : nat -> t +| C_128 : nat -> t +| C_129 : nat -> t +| C_130 : nat -> t +| C_131 : nat -> t +| C_132 : nat -> t +| C_133 : nat -> t +| C_134 : nat -> t +| C_135 : nat -> t +| C_136 : nat -> t +| C_137 : nat -> t +| C_138 : nat -> t +| C_139 : nat -> t +| C_140 : nat -> t +| C_141 : nat -> t +| C_142 : nat -> t +| C_143 : nat -> t +| C_144 : nat -> t +| C_145 : nat -> t +| C_146 : nat -> t +| C_147 : nat -> t +| C_148 : nat -> t +| C_149 : nat -> t +| C_150 : nat -> t +| C_151 : nat -> t +| C_152 : nat -> t +| C_153 : nat -> t +| C_154 : nat -> t +| C_155 : nat -> t +| C_156 : nat -> t +| C_157 : nat -> t +| C_158 : nat -> t +| C_159 : nat -> t +| C_160 : nat -> t +| C_161 : nat -> t +| C_162 : nat -> t +| C_163 : nat -> t +| C_164 : nat -> t +| C_165 : nat -> t +| C_166 : nat -> t +| C_167 : nat -> t +| C_168 : nat -> t +| C_169 : nat -> t +| C_170 : nat -> t +| C_171 : nat -> t +| C_172 : nat -> t +| C_173 : nat -> t +| C_174 : nat -> t +| C_175 : nat -> t +| C_176 : nat -> t +| C_177 : nat -> t +| C_178 : nat -> t +| C_179 : nat -> t +| C_180 : nat -> t +| C_181 : nat -> t +| C_182 : nat -> t +| C_183 : nat -> t +| C_184 : nat -> t +| C_185 : nat -> t +| C_186 : nat -> t +| C_187 : nat -> t +| C_188 : nat -> t +| C_189 : nat -> t +| C_190 : nat -> t +| C_191 : nat -> t +| C_192 : nat -> t +| C_193 : nat -> t +| C_194 : nat -> t +| C_195 : nat -> t +| C_196 : nat -> t +| C_197 : nat -> t +| C_198 : nat -> t +| C_199 : nat -> t +| C_200 : nat -> t +| C_201 : nat -> t +| C_202 : nat -> t +| C_203 : nat -> t +| C_204 : nat -> t +| C_205 : nat -> t +| C_206 : nat -> t +| C_207 : nat -> t +| C_208 : nat -> t +| C_209 : nat -> t +| C_210 : nat -> t +| C_211 : nat -> t +| C_212 : nat -> t +| C_213 : nat -> t +| C_214 : nat -> t +| C_215 : nat -> t +| C_216 : nat -> t +| C_217 : nat -> t +| C_218 : nat -> t +| C_219 : nat -> t +| C_220 : nat -> t +| C_221 : nat -> t +| C_222 : nat -> t +| C_223 : nat -> t +| C_224 : nat -> t +| C_225 : nat -> t +| C_226 : nat -> t +| C_227 : nat -> t +| C_228 : nat -> t +| C_229 : nat -> t +| C_230 : nat -> t +| C_231 : nat -> t +| C_232 : nat -> t +| C_233 : nat -> t +| C_234 : nat -> t +| C_235 : nat -> t +| C_236 : nat -> t +| C_237 : nat -> t +| C_238 : nat -> t +| C_239 : nat -> t +| C_240 : nat -> t +| C_241 : nat -> t +| C_242 : nat -> t +| C_243 : nat -> t +| C_244 : nat -> t +| C_245 : nat -> t +| C_246 : nat -> t +| C_247 : nat -> t +| C_248 : nat -> t +| C_249 : nat -> t +| C_250 : nat -> t +| C_251 : nat -> t +| C_252 : nat -> t +| C_253 : nat -> t +| C_254 : nat -> t +| C_255 : nat -> t +| C_256 : nat -> t. + +Definition is_256 (x : t) : bool := + match x with + | C_256 _ => true + | _ => false + end. + +Lemma falso : False. + assert (is_256 (C_256 0) = true) by reflexivity. + (* The next line was successful in 8.2pl3 *) + Fail assert (is_256 (C_256 0) = false) by (vm_compute; reflexivity). +Abort. diff --git a/test-suite/bugs/closed/bug_4366.v b/test-suite/bugs/closed/bug_4366.v deleted file mode 100644 index 403c2d2026..0000000000 --- a/test-suite/bugs/closed/bug_4366.v +++ /dev/null @@ -1,15 +0,0 @@ -Fixpoint stupid (n : nat) : unit := -match n with -| 0 => tt -| S n => - let () := stupid n in - let () := stupid n in - tt -end. - -Goal True. -Proof. -pose (v := stupid 24). -Timeout 4 vm_compute in v. -exact I. -Qed. diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v index 379e46b3e3..9b3210860c 100644 --- a/test-suite/bugs/closed/bug_4498.v +++ b/test-suite/bugs/closed/bug_4498.v @@ -19,6 +19,6 @@ Class Category := { Require Export Coq.Setoids.Setoid. -Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with +Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with signature equiv ==> equiv ==> equiv as compose_mor. Proof. apply comp_respects. Qed. diff --git a/test-suite/bugs/closed/bug_4509.v b/test-suite/bugs/closed/bug_4509.v new file mode 100644 index 0000000000..ceae7c5fc3 --- /dev/null +++ b/test-suite/bugs/closed/bug_4509.v @@ -0,0 +1,11 @@ +(* Was solved at some time, suspectingly in PR #6328 *) + +Goal exists n, n > 1. +Proof. + unshelve eexists. (*2 goals, as expected*) + Undo. + unshelve (eexists; instantiate (1:=ltac:(idtac))). (*only 1 goal*) + shelve. + Undo. + 2:unshelve instantiate (1:=_). +Abort. diff --git a/test-suite/bugs/closed/bug_4771.v b/test-suite/bugs/closed/bug_4771.v new file mode 100644 index 0000000000..e25e5a1be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_4771.v @@ -0,0 +1,21 @@ +(* The following code used to trigger an anomaly in functor substitutions *) + +Module Type Foo. + +Parameter Inline t : nat. + +End Foo. + +Module F(X : Foo). + +Tactic Notation "foo" ref(x) := idtac. + +Ltac g := foo X.t. + +End F. + +Module N. +Definition t := 0 + 0. +End N. + +Module K := F(N). diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v index 8b651ac22e..464a3de1b3 100644 --- a/test-suite/bugs/opened/bug_4781.v +++ b/test-suite/bugs/closed/bug_4781.v @@ -25,29 +25,29 @@ Goal True. let x := match constr:(Set) with ?y => constr:(y) end in pose x. (* This fails with an error: *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => constr:(y) end in pose x. (* The command has indeed failed with message: Error: Variable y should be bound to a term. *) (* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := match constr:(x) with ?y => y end in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := (eval cbv iota in x) in pose x. - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let x := type of x in pose x. (* should succeed *) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:(_ : abstract_term term) in let x := type of x in @@ -70,7 +70,7 @@ Even stranger, consider:*) (*This works fine. But if I change the period to a semicolon, I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -82,7 +82,7 @@ Even stranger, consider:*) (* should succeed *) (*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) - Fail let term := constr:(I) in + let term := constr:(I) in let T := type of term in let x := constr:((_ : abstract_term term) : T) in let y := (eval cbv iota in (let v : T := x in v)) in @@ -92,3 +92,5 @@ Even stranger, consider:*) let x := (eval cbv delta [x'] in x') in let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) idtac. (* should succeed *) + exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_4782.v b/test-suite/bugs/closed/bug_4782.v index be17a96f15..c08195d502 100644 --- a/test-suite/bugs/closed/bug_4782.v +++ b/test-suite/bugs/closed/bug_4782.v @@ -15,8 +15,8 @@ Record T := { dom : Type }. Definition pairT A B := {| dom := (dom A * dom B)%type |}. Class C (A:Type). Parameter B:T. -Instance c (A:T) : C (dom A). -Instance cn : C (dom B). +Instance c (A:T) : C (dom A) := {}. +Instance cn : C (dom B) := {}. Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. Set Typeclasses Debug. Goal forall (A:T) (x:dom A), pairT A A = pairT A A. diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v index 41a1251ca5..696812dee1 100644 --- a/test-suite/bugs/closed/bug_4798.v +++ b/test-suite/bugs/closed/bug_4798.v @@ -1,3 +1,5 @@ +(* DO NOT MODIFY THIS FILE DIRECTLY *) +(* It is autogenerated by dev/tools/update-compat.py. *) Check match 2 with 0 => 0 | S n => n end. Notation "|" := 1 (compat "8.7"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/bug_4811.v b/test-suite/bugs/closed/bug_4811.v deleted file mode 100644 index b90257cb3f..0000000000 --- a/test-suite/bugs/closed/bug_4811.v +++ /dev/null @@ -1,1686 +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 *) -Abort. diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v index 5838dcd8a7..9aefb10172 100644 --- a/test-suite/bugs/closed/bug_4836.v +++ b/test-suite/bugs/closed/bug_4836.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *) +(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *) diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index b67e93d677..0c236e12ad 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Primitive Projections. -Unset Printing Primitive Projection Compatibility. + Axiom Ω : Type. Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack { diff --git a/test-suite/bugs/closed/bug_5198.v b/test-suite/bugs/closed/bug_5198.v index 5d4409f89b..4f24189d3f 100644 --- a/test-suite/bugs/closed/bug_5198.v +++ b/test-suite/bugs/closed/bug_5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from diff --git a/test-suite/bugs/closed/bug_5401.v b/test-suite/bugs/closed/bug_5401.v index 95193b993b..466e669d00 100644 --- a/test-suite/bugs/closed/bug_5401.v +++ b/test-suite/bugs/closed/bug_5401.v @@ -5,7 +5,7 @@ Parameter P : nat -> Type. Parameter v : forall m, P m. Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0. Class U (R : P 0) (m : forall x, P x) : Prop. -Instance w : U (f _ (fun _ => v _)) v. +Instance w : U (f _ (fun _ => v _)) v := {}. Print HintDb typeclass_instances. End A. diff --git a/test-suite/bugs/closed/gh6165.v b/test-suite/bugs/closed/bug_6165.v index b87a7caaf2..b87a7caaf2 100644 --- a/test-suite/bugs/closed/gh6165.v +++ b/test-suite/bugs/closed/bug_6165.v diff --git a/test-suite/bugs/closed/bug_6202.v b/test-suite/bugs/closed/bug_6202.v new file mode 100644 index 0000000000..899260f59a --- /dev/null +++ b/test-suite/bugs/closed/bug_6202.v @@ -0,0 +1,11 @@ +(* This was fixed at some time, suspectingly in PR #6328 *) + +Inductive foo := F (a : forall var : Type -> Type, unit -> var unit) (_ : a = a). +Goal foo. + eexists (fun var => fun u : unit => ltac:(clear u)). + shelve. + Unshelve. + all:[ > | ]. + shelve. + Fail Grab Existential Variables. +Abort. diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/bug_6384.v index cec84642fb..cec84642fb 100644 --- a/test-suite/bugs/closed/gh6384.v +++ b/test-suite/bugs/closed/bug_6384.v diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/bug_6385.v index 3bbb664f4f..3bbb664f4f 100644 --- a/test-suite/bugs/closed/gh6385.v +++ b/test-suite/bugs/closed/bug_6385.v diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v index e88a3704d8..28a9ffc7bd 100644 --- a/test-suite/bugs/closed/bug_6661.v +++ b/test-suite/bugs/closed/bug_6661.v @@ -53,8 +53,6 @@ Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. exact x. Defined. -Unset Automatic Introduction. - Definition idfun (T : UU) := λ t:T, t. Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v index 34eb8b8676..93aeb83e28 100644 --- a/test-suite/bugs/closed/bug_7631.v +++ b/test-suite/bugs/closed/bug_7631.v @@ -7,6 +7,7 @@ Section Foo. Let bar := foo. Eval native_compute in bar. +Eval vm_compute in bar. End Foo. @@ -17,5 +18,6 @@ Module RelContext. Definition foo := true. Definition bar (x := foo) := Eval native_compute in x. +Definition barvm (x := foo) := Eval vm_compute in x. End RelContext. diff --git a/test-suite/bugs/closed/bug_7795.v b/test-suite/bugs/closed/bug_7795.v index 5db0f81cc5..5f9d42f5f7 100644 --- a/test-suite/bugs/closed/bug_7795.v +++ b/test-suite/bugs/closed/bug_7795.v @@ -52,6 +52,8 @@ Definition hh: false = true. Admitted. +Require Import Program. + Set Program Mode. (* removing this line prevents the bug *) Obligation Tactic := repeat t_base. diff --git a/test-suite/bugs/closed/bug_7811.v b/test-suite/bugs/closed/bug_7811.v index fee330f22d..155f3285b7 100644 --- a/test-suite/bugs/closed/bug_7811.v +++ b/test-suite/bugs/closed/bug_7811.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) +(* -*- mode: coq; coq-prog-args: ("-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) (* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *) (* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3 coqtop version 8.8.0 (May 2018) *) diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v new file mode 100644 index 0000000000..1e518e2adf --- /dev/null +++ b/test-suite/bugs/closed/bug_7904.v @@ -0,0 +1,13 @@ + + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances. + +Goal True. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *) + exact v. +Qed. diff --git a/test-suite/bugs/closed/bug_8076.v b/test-suite/bugs/closed/bug_8076.v new file mode 100644 index 0000000000..7bee43620f --- /dev/null +++ b/test-suite/bugs/closed/bug_8076.v @@ -0,0 +1,3 @@ + +Notation leak a := ltac:(let x := constr:(Type) in exact a) (only parsing). +Record foo@{} (P:leak Prop) := { f : leak Prop }. diff --git a/test-suite/bugs/closed/bug_8224.v b/test-suite/bugs/closed/bug_8224.v new file mode 100644 index 0000000000..42dd47d48c --- /dev/null +++ b/test-suite/bugs/closed/bug_8224.v @@ -0,0 +1,9 @@ +(* Checking that terms are evar-free before being grounded *) + +(* This used to raise an anomaly in 8.9 beta *) + +Fail Fixpoint restrict f n := + match n with + | O => nil + | S n => cons (f n) (restrict f n) + end. diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v new file mode 100644 index 0000000000..10f955b41f --- /dev/null +++ b/test-suite/bugs/closed/bug_8364.v @@ -0,0 +1,17 @@ +Unset Primitive Projections. + +Record Box (A:Type) := box { unbox : A }. +Arguments box {_} _. Arguments unbox {_} _. + +Definition map {A B} (f:A -> B) x := + match x with box x => box (f x) end. + +Definition tuple (l : Box Type) : Type := + match l with + | box x => x + end. + +Fail Inductive stack : Type -> Type := +| Stack T foos : + tuple (map stack foos) -> + stack T. diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_8544.v b/test-suite/bugs/closed/bug_8544.v new file mode 100644 index 0000000000..674d112595 --- /dev/null +++ b/test-suite/bugs/closed/bug_8544.v @@ -0,0 +1,6 @@ +Require Import ssreflect. +Goal True \/ True -> False. +Proof. +(* the following should fail: 2 subgoals, but only one intro pattern *) +Fail case => [a]. +Abort. diff --git a/test-suite/bugs/closed/bug_8755.v b/test-suite/bugs/closed/bug_8755.v new file mode 100644 index 0000000000..cd5aee4fa0 --- /dev/null +++ b/test-suite/bugs/closed/bug_8755.v @@ -0,0 +1,6 @@ + +Lemma f : Type. +Fail let i := ident:(i) in +let t := context i [Type] in +idtac. +Abort. diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v new file mode 100644 index 0000000000..9be1936cdf --- /dev/null +++ b/test-suite/bugs/closed/bug_8791.v @@ -0,0 +1,9 @@ +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. + +Definition A := 42. + +Instance foo (A: Type): Inhabited (list A). +Check A. +Abort. + +Fail Instance foo (A : nat) (A : Type) : Inhabited nat. diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v new file mode 100644 index 0000000000..5ff0b30260 --- /dev/null +++ b/test-suite/bugs/closed/bug_8794.v @@ -0,0 +1,11 @@ +(* This used to raise an anomaly in 8.8 *) + +Inductive T := Tau (t : T). + +Notation idT t := (match t with Tau t => Tau t end). + +Lemma match_itree : forall (t : T), t = idT t. +Proof. destruct t; auto. Qed. + +Lemma what (k : unit -> T) : k tt = k tt. +Proof. rewrite match_itree. Abort. diff --git a/test-suite/bugs/closed/bug_8819.v b/test-suite/bugs/closed/bug_8819.v new file mode 100644 index 0000000000..a4cb9dcd14 --- /dev/null +++ b/test-suite/bugs/closed/bug_8819.v @@ -0,0 +1,2 @@ +Theorem foo (_ : nat) (H : bool) : bool. +Proof. exact H. Qed. diff --git a/test-suite/bugs/closed/bug_8848.v b/test-suite/bugs/closed/bug_8848.v new file mode 100644 index 0000000000..26563e6747 --- /dev/null +++ b/test-suite/bugs/closed/bug_8848.v @@ -0,0 +1,18 @@ +Require Import Program. +Set Implicit Arguments. +Unset Strict Implicit. + +Definition def (a : nat) := a = a. + +Structure record {a : nat} {D : def a} := + inR { prop : Prop }. + +Program +Canonical Structure ins (a : nat) (rec : @record a _) := + @inR a _ (prop rec). +Next Obligation. + exact eq_refl. +Defined. +Next Obligation. + exact eq_refl. +Defined. diff --git a/test-suite/bugs/closed/bug_8885.v b/test-suite/bugs/closed/bug_8885.v new file mode 100644 index 0000000000..9d86c08d71 --- /dev/null +++ b/test-suite/bugs/closed/bug_8885.v @@ -0,0 +1,8 @@ +From Coq Require Import Cyclic31. + +Definition Nat `(int31) := nat. +Definition Zero (_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _: digits) := 0. + +Check (eq_refl (int31_rect Nat Zero 1) : 0 = 0). +Check (eq_refl (int31_rect Nat Zero 1) <: 0 = 0). +Check (eq_refl (int31_rect Nat Zero 1) <<: 0 = 0). diff --git a/test-suite/bugs/closed/bug_8908.v b/test-suite/bugs/closed/bug_8908.v new file mode 100644 index 0000000000..9c85839b75 --- /dev/null +++ b/test-suite/bugs/closed/bug_8908.v @@ -0,0 +1,8 @@ +Record foo : Type := + { fooA : Type; fooB : Type }. +Definition id {A : Type} (a : A) := a. +Definition untypable : Type. + unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y). + exact foo. + constructor. exact unit. exact unit. +Defined. diff --git a/test-suite/bugs/closed/bug_8951.v b/test-suite/bugs/closed/bug_8951.v new file mode 100644 index 0000000000..dce19318c5 --- /dev/null +++ b/test-suite/bugs/closed/bug_8951.v @@ -0,0 +1,14 @@ +Module Type T. + Polymorphic Parameter Inline t@{i} : Type@{i}. +End T. + +Module M. + Polymorphic Definition t@{i} := nat. +End M. + +Module Make (X:T). + Include X. + +End Make. + +Module P := Make M. diff --git a/test-suite/bugs/closed/bug_9014.v b/test-suite/bugs/closed/bug_9014.v new file mode 100644 index 0000000000..c1fdd04a65 --- /dev/null +++ b/test-suite/bugs/closed/bug_9014.v @@ -0,0 +1,19 @@ +(* A type, not a class *) +Variant T := mkT. + +(* In records, :> declares a coercion *) +Record R := { t_of_r :> T }. +Check forall r : R, r = r :> T. + +(* A class *) +Class A := { p : Prop }. +(* A sub-class *) +Class B := { a_of_b :> A ; t_of_b :> T }. +(* The sub-instance is automatically inferred due to :> for a_of_b *) +Check forall b : B, p. +(* No coercion is introduced by :> in t_of_b *) +Fail Check forall b : B, b = b :> T. + +(* Using :> when the RHS is not a class produces a “not-a-class” warning. *) +Set Warnings "+not-a-class". +Fail Class B' := { a_of_b' :> A ; t_of_b' :> T }. diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v new file mode 100644 index 0000000000..a89837dd12 --- /dev/null +++ b/test-suite/bugs/closed/bug_9166.v @@ -0,0 +1,11 @@ +(* DO NOT MODIFY THIS FILE DIRECTLY *) +(* It is autogenerated by dev/tools/update-compat.py. *) +Set Warnings "+deprecated". + +Notation bar := option (compat "8.7"). + +Definition foo (x: nat) : nat := + match x with + | 0 => 0 + | S bar => bar + end. diff --git a/test-suite/bugs/closed/bug_9229.v b/test-suite/bugs/closed/bug_9229.v new file mode 100644 index 0000000000..7514741af4 --- /dev/null +++ b/test-suite/bugs/closed/bug_9229.v @@ -0,0 +1,6 @@ +(* There was a problem of freshness with Infix choice of vars *) + +(* In particular, x and y were special... *) + +Infix "#" := (fun x y => x + y) (at level 50, left associativity). +Check (3 # 5). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) diff --git a/test-suite/bugs/closed/bug_9268.v b/test-suite/bugs/closed/bug_9268.v new file mode 100644 index 0000000000..02dd46f6d2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9268.v @@ -0,0 +1,46 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. + +Local Open Scope Z_scope. + +Definition Register := Z%type. + +Definition Opcode := Z%type. + +Inductive InstructionI : Type + := Lb : Register -> Register -> Z -> InstructionI + | InvalidI : InstructionI. + +Inductive Instruction : Type + := IInstruction : InstructionI -> Instruction. + +Definition funct3_LB : Z := 0. + +Definition opcode_LOAD : Opcode := 3. + +Set Universe Polymorphism. + +Definition MachineInt := Z. + +Definition funct3_JALR := 0. + +Axiom InstructionMapper: Type -> Type. + +Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z := + match inst with + | IInstruction InvalidI => 2 + | IInstruction (Lb rd rs1 oimm12) => 3 + end. + +Axiom Encoder: InstructionMapper MachineInt. + +Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder. + +Lemma foo: forall (ins: InstructionI), + 0 <= encode (IInstruction ins) -> + 0 <= encode (IInstruction ins) . +Proof. + Set Printing Universes. + intros. + lia. +Qed. diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). diff --git a/test-suite/bugs/closed/bug_9313.v b/test-suite/bugs/closed/bug_9313.v new file mode 100644 index 0000000000..0845e7732c --- /dev/null +++ b/test-suite/bugs/closed/bug_9313.v @@ -0,0 +1,13 @@ +Set Implicit Arguments. +Existing Class True. + +Instance foo1 (a : nat) {b : nat} (e : a = b) : True := I. +Check foo1 (a := 3) (b := 4). + +Definition foo2 (a : nat) {b : nat} (e : a = b) : True := I. +Check foo2 (a := 3) (b := 4). + +Instance foo3 (a : nat) {b : nat} (e : a = b) : True. +exact I. +Qed. +Check foo3 (a := 3) (b := 4). diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v new file mode 100644 index 0000000000..c0322dec40 --- /dev/null +++ b/test-suite/bugs/closed/bug_9329.v @@ -0,0 +1,12 @@ +(* Declare empty levels in the same order they are computed *) + +Notation "< a ; b ; c >1" := + (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21). +Notation "< a ; b ; c >2" := + (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31). +Notation "< a ; b ; c >3" := + (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41). +Notation "< a ; b ; c >4" := + (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49). +Notation "< a ; b >" := + (sum a b) (at level 61, a at level 63, b at level 62). diff --git a/test-suite/bugs/closed/bug_9363.v b/test-suite/bugs/closed/bug_9363.v new file mode 100644 index 0000000000..a3f6ad9fa2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9363.v @@ -0,0 +1,17 @@ +(* Outside a section, Hypothesis, Variable, Axiom all obey implicit binders *) +Hypothesis foo1 : forall {n : nat}, True. +Variable foo1' : forall {n : nat}, True. +Axiom foo1'' : forall {n : nat}, True. +Check foo1 (n := 1). +Check foo1' (n := 1). +Check foo1'' (n := 1). + +Section bar. +(* Inside a section, Hypothesis and Variable do not, but they should *) +Hypothesis foo2 : forall {n : nat}, True. +Variable foo2' : forall {n : nat}, True. +Axiom foo2'' : forall {n : nat}, True. +Check foo2 (n := 1). +Check foo2' (n := 1). +Check foo2'' (n := 1). +End bar. diff --git a/test-suite/bugs/closed/bug_9367.v b/test-suite/bugs/closed/bug_9367.v new file mode 100644 index 0000000000..885f6bc391 --- /dev/null +++ b/test-suite/bugs/closed/bug_9367.v @@ -0,0 +1,12 @@ +Section foo. +Variable f : forall n : nat, nat. +Arguments f {_}. +Check f (n := 3). +Global Arguments f {bar} : rename. +End foo. + +Section foo. +Variable f : forall n : nat, nat. +Arguments f {_}. +Fail Check f (bar := 3). +End foo. diff --git a/test-suite/bugs/closed/bug_9375.v b/test-suite/bugs/closed/bug_9375.v new file mode 100644 index 0000000000..a2bfbafe06 --- /dev/null +++ b/test-suite/bugs/closed/bug_9375.v @@ -0,0 +1,16 @@ +Set Primitive Projections. + +Record toto : Type := Toto { + toto1 : Type; + toto2 : toto1 -> Type +}. + +Record tata := Tata { + tata1 : Type +}. + +Canonical Structure tata_toto (x : toto) X := + Tata (toto2 x X). + +Check fun (T : toto) (t : toto1 T) => + (eq_refl _ : @tata1 _ = @toto2 _ t). diff --git a/test-suite/bugs/closed/bug_9432.v b/test-suite/bugs/closed/bug_9432.v new file mode 100644 index 0000000000..c85f8129ce --- /dev/null +++ b/test-suite/bugs/closed/bug_9432.v @@ -0,0 +1,12 @@ + +Record foo := { f : Type }. + +Fail Canonical Structure xx@{} := {| f := Type |}. + +Canonical Structure xx@{i} := {| f := Type@{i} |}. + +Fail Coercion cc@{} := fun x : Type => Build_foo x. + +Polymorphic Coercion cc@{i} := fun x : Type@{i} => Build_foo x. + +Coercion cc1@{i} := (cc@{i}). diff --git a/test-suite/bugs/closed/bug_9451.v b/test-suite/bugs/closed/bug_9451.v new file mode 100644 index 0000000000..03bb0433f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_9451.v @@ -0,0 +1,8 @@ +Goal False. +cut True. +assert False. +evar (x : True). +let v := open_constr:(_) in idtac. all: exfalso; clear. +Optimize Proof. +(* Error: Anomaly "grounding a non evar-free term" *) +Abort All. diff --git a/test-suite/bugs/closed/bug_9453.v b/test-suite/bugs/closed/bug_9453.v new file mode 100644 index 0000000000..18745533b2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9453.v @@ -0,0 +1,7 @@ +(* check compatibility with 8.8 and earlier for lack of warnings on the nat 5000 *) +Set Warnings Append "+large-nat,+abstract-large-number". +Fail Check 5001. +Check 5000. +(* Error: +To avoid stack overflow, large numbers in nat are interpreted as applications of +Nat.of_uint. *) diff --git a/test-suite/bugs/closed/bug_9494.v b/test-suite/bugs/closed/bug_9494.v new file mode 100644 index 0000000000..a0b8383d16 --- /dev/null +++ b/test-suite/bugs/closed/bug_9494.v @@ -0,0 +1,10 @@ +Lemma foo (a : nat) : True. +Proof. +destruct a eqn:n; exact I. +Qed. + +Set Mangle Names. +Lemma foo2 (a : nat) : True. +Proof. +let N := fresh in destruct a eqn:N; exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_9508.v b/test-suite/bugs/closed/bug_9508.v new file mode 100644 index 0000000000..2c38e24add --- /dev/null +++ b/test-suite/bugs/closed/bug_9508.v @@ -0,0 +1,29 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Module OK. +Record A := mkA { + T : Type; + P : T -> bool; +}. + +About P. (* Argument a is implicit *) +Check P (true: T (mkA negb)). +End OK. + +Module KO. +Set Primitive Projections. +Record A := mkA { + T : Type; + P : T -> bool; +}. + +About P. (* No implicit arguments *) +Check P (true: T (mkA negb)). +(* +The command has indeed failed with message: +The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}" +while it is expected to have type "A". +*) + +End KO. diff --git a/test-suite/bugs/closed/bug_9526.v b/test-suite/bugs/closed/bug_9526.v new file mode 100644 index 0000000000..344d42083f --- /dev/null +++ b/test-suite/bugs/closed/bug_9526.v @@ -0,0 +1,30 @@ +Primitive int := #int63_type. + +Module bad1. +Polymorphic Inductive badcarry1 (A:Type) : Type := +| C0: A -> badcarry1 A +| C1: A -> badcarry1 A. + +Fail Register badcarry1 as kernel.ind_carry. + +End bad1. + +Module bad2. + +Inductive badcarry2 (A:Set) : Set := +| C0: A -> badcarry2 A +| C1: A -> badcarry2 A. + +Fail Register badcarry2 as kernel.ind_carry. + +End bad2. + +Module bad3. + +Inductive badcarry3 : Type -> Type := +| C0: forall A, A -> badcarry3 A +| C1: forall A, A -> badcarry3 A. + +Fail Register badcarry3 as kernel.ind_carry. + +End bad3. diff --git a/test-suite/bugs/closed/bug_9527.v b/test-suite/bugs/closed/bug_9527.v new file mode 100644 index 0000000000..e08d194c6c --- /dev/null +++ b/test-suite/bugs/closed/bug_9527.v @@ -0,0 +1 @@ +Fail Check fix f (x : nat) := (let x := (f x) in f 0). diff --git a/test-suite/bugs/closed/bug_9595.v b/test-suite/bugs/closed/bug_9595.v new file mode 100644 index 0000000000..312ed7d045 --- /dev/null +++ b/test-suite/bugs/closed/bug_9595.v @@ -0,0 +1,11 @@ +Set Primitive Projections. +Set Warnings "+non-primitive-record". + +(* 0 fields *) +Fail Record foo := { a := 0 }. + +(* anonymous field *) +Fail Record foo := { _ : nat }. + +(* squashed *) +Fail Record foo : Prop := { a : nat }. diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v new file mode 100644 index 0000000000..00bbfcf5d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9598.v @@ -0,0 +1,36 @@ +Module case. + + Inductive pair := K (n1 : nat) (n2 : nat). + Definition fst (p : pair) : nat := match p with K n _ => n end. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End case. + +Module fixpoint. + + Inductive pair := K (n1 : nat) (n2 : nat). + Fixpoint fst (p : pair) : nat := match p with K n _ => n end. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End fixpoint. + +Module primproj. + + Set Primitive Projections. + + Inductive pair := K { fst : nat; snd : nat }. + + Definition alias_K a b := K a b. + + Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)). + Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)). + +End primproj. diff --git a/test-suite/bugs/closed/bug_9631.v b/test-suite/bugs/closed/bug_9631.v new file mode 100644 index 0000000000..8afeccccd4 --- /dev/null +++ b/test-suite/bugs/closed/bug_9631.v @@ -0,0 +1,7 @@ + +Fail Instance x : _. + +Existing Class True. +(* the type is checked for typeclass-ness before interping the body so + this is the same error *) +Fail Instance x : _ := I. diff --git a/test-suite/bugs/closed/bug_9663.v b/test-suite/bugs/closed/bug_9663.v new file mode 100644 index 0000000000..b5fa601278 --- /dev/null +++ b/test-suite/bugs/closed/bug_9663.v @@ -0,0 +1,2 @@ +Definition id_depfn S T (f : forall x : S, T x) := f. +Definition idn : nat -> nat := @id_depfn _ _ (fun x => x). diff --git a/test-suite/bugs/closed/bug_sprop_13.v b/test-suite/bugs/closed/bug_sprop_13.v new file mode 100644 index 0000000000..ae80c9c51f --- /dev/null +++ b/test-suite/bugs/closed/bug_sprop_13.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *) +Goal forall (P : SProp), P -> P. +Proof. + intros P H. set (H0 := H). + (* goal is now H0 *) + exact H0. +Qed. diff --git a/test-suite/bugs/closed/bug_sprop_14.v b/test-suite/bugs/closed/bug_sprop_14.v new file mode 100644 index 0000000000..1e6e9b30de --- /dev/null +++ b/test-suite/bugs/closed/bug_sprop_14.v @@ -0,0 +1,26 @@ +(* -*- coq-prog-args: ("-allow-sprop"); -*- *) + +Set Universe Polymorphism. + +Inductive False : SProp :=. + +Axiom ℙ@{} : SProp. + +Definition TYPE@{i} := ℙ -> Type@{i}. +Definition PROP@{} := ℙ -> SProp. + +Definition El@{i} (A : TYPE@{i}) := forall p, A p. +Definition sEl@{} (A : PROP@{}) : SProp := forall p, A p. + +Definition SPropᶠ@{} := fun (p : ℙ) => SProp. + +Definition sProdᶠ@{i} + (A : TYPE@{i}) + (B : forall (p : ℙ), El A -> SProp) : PROP := fun (p : ℙ) => forall x : El A, B p x. + +Definition Falseᶠ : El SPropᶠ := fun p => False. + +Definition EMᶠ : sEl (sProdᶠ SPropᶠ (fun p A => ((sProdᶠ A (fun p _ => Falseᶠ p))) p)). +Proof. +Fail Admitted. +Abort. diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v index e1c29a954c..baf87631f0 100644 --- a/test-suite/bugs/opened/bug_3166.v +++ b/test-suite/bugs/opened/bug_3166.v @@ -81,3 +81,4 @@ Goal forall T (x y : T) (p : x = y), True. compute in H0. change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. Fail pose proof (fun k => @eq_trans _ _ _ k H0). +Abort. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v index a717bbe735..18820b1a4c 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/opened/bug_3754.v @@ -282,3 +282,4 @@ Defined. rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. Fail rewrite (concat_Ap ff2). + Abort. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v index 5c74addb62..9d83743b2a 100644 --- a/test-suite/bugs/opened/bug_3890.v +++ b/test-suite/bugs/opened/bug_3890.v @@ -1,7 +1,11 @@ +Set Nested Proofs Allowed. + Class Foo. Class Bar := b : Type. +Set Refine Instance Mode. Instance foo : Foo := _. +Unset Refine Instance Mode. (* 1 subgoals, subgoal 1 (ID 4) ============================ diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v index 2d0d1930f1..3c7c945ed8 100644 --- a/test-suite/bugs/opened/bug_3938.v +++ b/test-suite/bugs/opened/bug_3938.v @@ -4,3 +4,4 @@ Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. intros a b f H. rewrite H. (* Toplevel input, characters 15-25: Anomaly: Evar ?X11 was not declared. Please report. *) +Abort. |