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: 0.4.95@7852~822 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8bf2443a45a06c53153344201213afab724bf142;p=helm.git Added more typing information to remove a coercion. --- diff --git a/matita/dama/reals.ma b/matita/dama/reals.ma index dbd4fa01e..97ca4151f 100644 --- a/matita/dama/reals.ma +++ b/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