aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Scheme.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index 4b928007cf..273cb48295 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -18,7 +18,7 @@ Check myeq_rew.
Check myeq_rew_dep.
Check myeq_rew_fwd_dep.
Check myeq_rew_r.
-Check internal_myeq_sym_involutive.
+Check myeq_sym_involutive.
Check myeq_rew_r_dep.
Check myeq_rew_fwd_r_dep.