diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-22 06:44:14 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-22 06:44:14 +0000 |
| commit | 353e280be1006b646cb4ac53e7282b4fe19b0460 (patch) | |
| tree | 2ad5d5d780fb267e57644961a3bcf4a27f7923be /test-suite/success/setoid_ring_module.v | |
| parent | 583a1fe9e37c87ad56c16b4c384bf9dccf48224d (diff) | |
remove an orphan comment (attached to a piece of code that was removed).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9072 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/setoid_ring_module.v')
| -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 661f17878..9dfedce35 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. |