diff options
Diffstat (limited to 'theories/Arith/Peano_dec.v')
| -rw-r--r-- | theories/Arith/Peano_dec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index e68ba9590..e121ce30d 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -29,7 +29,7 @@ Defined. Hint Resolve O_or_S eq_nat_dec: arith. Theorem dec_eq_nat : forall n m, decidable (n = m). - intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith. + intros x y; unfold decidable; elim (eq_nat_dec x y); auto with arith. Defined. Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec. |