diff options
Diffstat (limited to 'theories/Arith/Peano_dec.v')
| -rw-r--r-- | theories/Arith/Peano_dec.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 9a24c804a1..ddbc128aa1 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -30,6 +30,8 @@ Proof. elim (Nat.eq_dec n m); [left|right]; trivial. Defined. +Register dec_eq_nat as num.nat.eq_dec. + Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec. Import EqNotations. |