From 662ca19ed7dabecdf17cdd555132f106bb768e58 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Thu, 7 Apr 2022 17:58:39 +0100
Subject: Add a new ring solver tactic.

---
 Everything.agda | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Everything.agda')

diff --git a/Everything.agda b/Everything.agda
index 039338b..cd0f148 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -125,3 +125,6 @@ import Helium.Semantics.Axiomatic.Triple
 
 -- Base definitions for the denotational semantics.
 import Helium.Semantics.Denotational.Core
+
+-- Ring solver tactic using integers as coefficients
+import Helium.Tactic.CommutativeRing.NonReflective
-- 
cgit v1.2.3