From 45959b9960b6f3b588dfeef83da17212f5a09763 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 6 Dec 2018 13:41:31 -0800
Subject: [PATCH] Remove rules ecEq_unfold and ecEq_refl.

(Proofs can now use `add_cryptol_defs ["ecEq"]` instead.)
---
 saw/Cryptol.sawcore | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/saw/Cryptol.sawcore b/saw/Cryptol.sawcore
index 3d7f2a244c..43ac97a682 100644
--- a/saw/Cryptol.sawcore
+++ b/saw/Cryptol.sawcore
@@ -1284,11 +1284,6 @@ ecSle =
 --------------------------------------------------------------------------------
 -- Rewrite rules
 
-ecEq_unfold : (a : sort 0) -> (pa : PCmp a) -> Eq (a -> a -> Bool) (ecEq a pa) pa.eq;
-ecEq_unfold a pa = Refl (a -> a -> Bool) (ecEq a pa);
-
-axiom ecEq_refl : (a : sort 0) -> (pa : PCmp a) -> (x : a) -> Eq Bool (ecEq a pa x x) True;
-
 axiom replicate_False : (n : Nat) -> Eq (bitvector n) (replicate n Bool False) (bvNat n 0);
 
 axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;