aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/test/custom/Ranalysis
diff options
context:
space:
mode:
authorletouzey2002-03-21 17:06:15 +0000
committerletouzey2002-03-21 17:06:15 +0000
commit88ff300b20833b71ec5d31fffcc766dda9aba365 (patch)
treea45d404db9d74762f3b21e46485ec498b26695b8 /contrib/extraction/test/custom/Ranalysis
parent04117381b1130ed2cde716c7b80f34e625b9b276 (diff)
reparation du test des reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/custom/Ranalysis')
-rw-r--r--contrib/extraction/test/custom/Ranalysis2
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/extraction/test/custom/Ranalysis b/contrib/extraction/test/custom/Ranalysis
new file mode 100644
index 0000000000..d8f1b3e7b7
--- /dev/null
+++ b/contrib/extraction/test/custom/Ranalysis
@@ -0,0 +1,2 @@
+Load "custom/Reals".
+