aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/README
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/README')
-rw-r--r--plugins/cc/README2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/README b/plugins/cc/README
index c616b5daab..7df7b971e8 100644
--- a/plugins/cc/README
+++ b/plugins/cc/README
@@ -9,7 +9,7 @@ Files :
- ccalgo.ml : congruence closure algorithm
- ccproof.ml : proof generation code
-- cctac.ml4 : the tactic itself
+- cctac.mlg : the tactic itself
- CCSolve.v : a small Ltac tactic based on congruence
Known Bugs : the congruence tactic can fail due to type dependencies.