From 7ea6628e47d158e598205e246df3d387a08e7e82 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 5 Nov 2006 10:14:04 +0000 Subject: [PATCH] Added more typing information to remove a coercion. --- helm/software/matita/dama/reals.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2