From c86d78c0f18fb28f74bb6b192c03ebe73117cf03 Mon Sep 17 00:00:00 2001 From: bgregoir Date: Mon, 11 Dec 2006 18:46:35 +0000 Subject: Changement dans le kernel : - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rfunctions.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'theories/Reals/Rfunctions.v') diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index f048faf53..ba7396ed6 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -19,6 +19,7 @@ Require Export LegacyArithRing. (* for ring_nat... *) Require Export ArithRing. Require Import Rbase. +Require Export Rpow_def. Require Export R_Ifp. Require Export Rbasic_fun. Require Export R_sqr. @@ -65,11 +66,6 @@ Qed. (** * Power *) (*******************************) (*********) -Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := - match n with - | O => 1 - | S n => r * pow r n - end. Infix "^" := pow : R_scope. -- cgit v1.2.3