1 files changed, 6 insertions, 0 deletions
diff --git a/src/Galois/ComputationalGaloisField.v b/src/Galois/ComputationalGaloisField.v
index a17783475..e83e22fea 100644
--- a/src/Galois/ComputationalGaloisField.v
+++ b/src/Galois/ComputationalGaloisField.v
@@ -37,6 +37,12 @@ Module ComputationalGaloisField (M: Modulus).
     | _ => t
     end.
 
+  Add Ring GFring_computational : GFring_theory
+    (decidable GFdecidable,
+     constants [GFconstants],
+     div GFdiv_theory,
+     power_tac GFpower_theory [GFexp_tac]).
+
   Add Field GFfield_computational : GFfield_theory
     (decidable GFdecidable,
      completeness GFcomplete,