From 00d4c83968f17bb302af61d6fa9160c944e68b29 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 17 Sep 2014 15:28:46 +0200
Subject: Change an axiom into a definition.

---
 theories/Reals/Ranalysis_reg.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'theories/Reals')

diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
index a4b18288a..96865b3ff 100644
--- a/theories/Reals/Ranalysis_reg.v
+++ b/theories/Reals/Ranalysis_reg.v
@@ -28,7 +28,10 @@ Require Export Ranalysis4.
 Require Export Rpower.
 Local Open Scope R_scope.
 
-Axiom AppVar : R.
+Definition AppVar : R.
+Proof.
+exact R0.
+Qed.
 
 (**********)
 Ltac intro_hyp_glob trm :=
-- 
cgit v1.2.3