From 0667c8e4bfd796f6e42c97041ab9d48236791d3b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 May 2003 01:33:26 +0000
Subject: Amelioration affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4019 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Arith/Factorial.v  | 2 ++
 theories/Reals/Rfunctions.v | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 71cef55ce4..ca176a6c67 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -22,6 +22,8 @@ Fixpoint fact [n:nat]:nat:=
     |(S n) => (mult (S n) (fact n))
   end.
 
+Arguments Scope fact [ nat_scope ].
+
 Lemma lt_O_fact : (n:nat)(lt O (fact n)).
 Proof.
 Induction n; Unfold lt; Simpl; Auto with arith.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 7d8e4b02cb..220e3919bc 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -66,6 +66,8 @@ Fixpoint pow [r:R;n:nat]:R:=
     |(S n) => (Rmult r (pow r n))
   end.
 
+Arguments Scope pow [ R_scope nat_scope ].
+
 Lemma pow_O: (e : R)  (pow e O) == R1.
 Simpl; Auto with real.
 Qed.
-- 
cgit v1.2.3