make the opam package meta data

1 files changed, 7 insertions, 0 deletions

diff --git a/mathcomp/real_closed/descr b/mathcomp/real_closed/descr
new file mode 100644
index 0000000..b51ecf9
--- /dev/null
+++ b/mathcomp/real_closed/descr
@@ -0,0 +1,7 @@
+Mathematical Components Library on real closed fields
+
+This library contains definitions and theorems about real closed
+fields, with a construction of the real closure and the algebraic
+closure (including a proof of the fundamental theorem of algebra). It
+also contains a proof of decidability of the first order theory of
+real closed field, through quantifier elimination.