summaryrefslogtreecommitdiff
path: root/src/util/stats_timer.h
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-04-01 09:56:14 -0700
committerGitHub <noreply@github.com>2021-04-01 16:56:14 +0000
commit05a53a2ac405bcd18a84024247145f161809c3b0 (patch)
tree34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/util/stats_timer.h
parentafaf4413775ff7d6054a5893f1397ad908e0773c (diff)
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/util/stats_timer.h')
-rw-r--r--src/util/stats_timer.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h
index 40df52ade..92ea87b59 100644
--- a/src/util/stats_timer.h
+++ b/src/util/stats_timer.h
@@ -24,7 +24,7 @@
#include "cvc4_export.h"
#include "util/stats_base.h"
-namespace CVC5 {
+namespace cvc5 {
namespace timer_stat_detail {
using clock = std::chrono::steady_clock;
using time_point = clock::time_point;
@@ -46,7 +46,7 @@ class CodeTimer;
class CVC4_EXPORT TimerStat : public BackedStat<timer_stat_detail::duration>
{
public:
- typedef CVC5::CodeTimer CodeTimer;
+ typedef cvc5::CodeTimer CodeTimer;
/**
* Construct a timer statistic with the given name. Newly-constructed
@@ -108,6 +108,6 @@ private:
CodeTimer& operator=(const CodeTimer& timer) = delete;
}; /* class CodeTimer */
-} // namespace CVC5
+} // namespace cvc5
#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback