From 71110a218f69a69010adde2f296e4022ef94b755 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 May 2019 17:27:08 +0200 Subject: Modifying theories to preferably use the "[= ]" syntax, and, sometimes, to use "intros [= ...]" rather than things like "intros H; injection H as [= ...]". Co-Authored-By: Théo Zimmermann --- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Numbers/Cyclic/ZModulo/ZModulo.v') diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 4bcd22543f..94da55b3f3 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -372,7 +372,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H as ? ?. + destruct 1; injection H as [= ? ?]. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -414,7 +414,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1 as ? ?. + injection H1 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -525,7 +525,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4 as ? ?. + injection H4 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. -- cgit v1.2.3