From 8bf2443a45a06c53153344201213afab724bf142 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 5 Nov 2006 10:14:04 +0000
Subject: [PATCH] Added more typing information to remove a coercion.

---
 matita/dama/reals.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
2.39.2