diff options
| -rw-r--r-- | test-suite/success/setoid_ring_module.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/success/setoid_ring_module.v b/test-suite/success/setoid_ring_module.v index 661f17878e..9dfedce35e 100644 --- a/test-suite/success/setoid_ring_module.v +++ b/test-suite/success/setoid_ring_module.v @@ -30,10 +30,6 @@ Admitted. Add New Ring CoefRing : cRth Abstract. -(* Here the tactic that I would like to be implemented by - "setoid ring" when it is applied on a "ceq _ _" goal. - This tactic was designed by copying what happens in newring.ml4 *) - End abs_ring. Import abs_ring. |