From: Claudio Sacerdoti Coen Date: Sun, 5 Nov 2006 10:14:04 +0000 (+0000) Subject: Added more typing information to remove a coercion. X-Git-Tag: make_still_working~6681 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ea6628e47d158e598205e246df3d387a08e7e82;p=helm.git Added more typing information to remove a coercion. --- diff --git a/helm/software/matita/dama/reals.ma b/helm/software/matita/dama/reals.ma index dbd4fa01e..97ca4151f 100644 --- a/helm/software/matita/dama/reals.ma +++ b/helm/software/matita/dama/reals.ma @@ -121,4 +121,4 @@ definition max: ∀R:real.R → R → R. apply cauchy_max_seq. qed. -definition abs \def λR.λx:Type_OF_real R. max R x (-x). \ No newline at end of file +definition abs \def λR:real.λx:R. max R x (-x). \ No newline at end of file