diff options
Diffstat (limited to 'theories/Numbers/Integer/BigZ/ZMake.v')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index d1c817f54..6b4e154c0 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -416,7 +416,7 @@ Module Make (NN:NType) <: ZType. Ltac break_nonneg x px EQx := let H := fresh "H" in assert (H:=NN.spec_pos x); - destruct (NN.to_Z x) as [|px|px]_eqn:EQx; + destruct (NN.to_Z x) as [|px|px] eqn:EQx; [clear H|clear H|elim H; reflexivity]. Theorem spec_div_eucl: forall x y, |