summaryrefslogtreecommitdiff
path: root/src/util/floatingpoint.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/floatingpoint.h')
-rw-r--r--src/util/floatingpoint.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index 060d1de99..e038959a0 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -29,7 +29,7 @@
/* -------------------------------------------------------------------------- */
-namespace CVC5 {
+namespace cvc5 {
/* -------------------------------------------------------------------------- */
@@ -514,7 +514,7 @@ struct FloatingPointToBVHashFunction
{
inline size_t operator()(const FloatingPointToBV& fptbv) const
{
- UnsignedHashFunction< ::CVC5::BitVectorSize> f;
+ UnsignedHashFunction< ::cvc5::BitVectorSize> f;
return (key ^ 0x46504256) ^ f(fptbv.d_bv_size);
}
}; /* struct FloatingPointToBVHashFunction */
@@ -533,6 +533,6 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps);
std::ostream& operator<<(std::ostream& os,
const FloatingPointConvertSort& fpcs);
-} // namespace CVC5
+} // namespace cvc5
#endif /* CVC4__FLOATINGPOINT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback