diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | theories/Reals/Reals.v | 1 |
2 files changed, 3 insertions, 1 deletions
@@ -449,7 +449,8 @@ REALSVO=theories/Reals/TypeSyntax.vo \ theories/Reals/SplitRmult.vo theories/Reals/Rfunctions.vo \ theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo \ theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo \ - theories/Reals/R_sqr.vo theories/Reals/Reals.vo + theories/Reals/R_sqr.vo theories/Reals/Rsigma.vo \ + theories/Reals/Reals.vo SETOIDSVO=theories/Setoids/Setoid.vo diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 473930c765..15b4fb2db4 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -15,6 +15,7 @@ Require Export Rbase. Require Export R_Ifp. Require Export Rbasic_fun. Require Export R_sqr. +Require Export Rsigma. Require Export Rlimit. Require Export Rfunctions. Require Export Rderiv. |