aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/BigN/BigN.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ec1017f50..e8ff516f3 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -110,7 +110,7 @@ intros NEQ.
generalize (BigN.spec_div_eucl a b).
generalize (Z_div_mod_full [a] [b] NEQ).
destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
BigN.zify. rewrite EQr, EQq; auto.
Qed.